***  late attempt at using this
*** as a simple running example to illustrate a bunch
*** of things.  Yes, it is simple, but maybe because of that
*** it could be useful:


omod FIG7 is
  including LF-REPR .
  protecting LF-VALUE-TIME .
 
  op s : -> RVarId [ctor] .
  ops relay x y : -> ReactorId [ctor] .
  ops inc dbl r out : -> RPortId [ctor] .
  op startup : -> RActionId .
  op init : -> Configuration .
 
  eq init = 
 
     < x : Reactor | 
       inports : < dbl : Port | value : [0] > 
                  < inc : Port | value : [0] >,
       outports : none, 
       state : s |-> [1],
       timers : none,
       actions : none,
       reactions : 
         (reaction when dbl do { s := s + s })
         reaction when inc  do { s := s + [1] }
     >
 
     < relay : Reactor | 
       inports : < r : Port | value : [0] >,
       outports : < out : Port | value : [0] >, 
       state : empty,
       timers : none,
       actions : none,
       reactions : 
         reaction when r --> out do { out <- r }
     >
     < y : Reactor | 
       inports : none,
       outports : < dbl : Port | value : [0] > 
                  < inc : Port | value : [0] >, 
       state : empty,
       timers : none,
       actions : < startup : LogicalAction | minDelay : 0, 
                                minSpacing : 0, 
                                policy : defer, 
                                payload : [0] >,
       reactions : 
         reaction when startup --> dbl ; inc do {(dbl <- [1]) ; (inc <- [1])}
     >
 
    (y : dbl --> relay : r)
    (relay : out --> x : dbl)
    (y : inc --> x : inc) .
 endom
 
 
 
 omod TEST-FIG7 is
   including FIG7 .
   including DYNAMICS-WITHOUT-TICK .
 
   ops env queue rxns : -> Oid [ctor] .
 
   op initSystem : -> GlobalSystem .
   eq initSystem =
       {< env : Environment | physicalActions : none >
        addReactionIndices(init)
        < queue : EventQueue | queue : addStartup(startup, init, empty) >
        < rxns : Invoked | reactions : none >} .
 endom
 
 
 omod SIMULATE-FIG7 is
   including TEST-FIG7 .
   including SIMULATION-DYNAMICS .
 endom  
 
 red initSystem .
 
 
 
 
 rew [33] initSystem .
 
 omod UNCLOCKED-FIG7 is
   including TEST-FIG7 .
   including UNBOUNDED-ANALYSIS-DYNAMICS  .
 
   op valueOf_._in_ : ReactorId VarId GlobalSystem -> Value [frozen (3)]
 .
   op valueOf_._in_ : ReactorId VarId ClockedSystem -> Value [frozen (3)]
 .
 
   var VAR : VarId .   var REACTOR : ReactorId .   var RS : ReactorState .
   var CONF : Configuration .   var ATTS : AttributeSet .  var T : Time .
   var SYSTEM : GlobalSystem .  var VALUE : Value .
 
 eq valueOf REACTOR . VAR in
       {CONF < REACTOR : Reactor | state : ((VAR |-> VALUE) ; RS),
       ATTS:AttributeSet >} = VALUE .
 
 eq valueOf REACTOR . VAR in SYSTEM in time T
  = valueOf REACTOR . VAR in SYSTEM .
 
 endom  
 
 rew [33] initSystem .
 
 
 search [1] initSystem =>*  {REST:Configuration
                             < x : Reactor | state : (s |-> [2]), ATTS:AttributeSet >} .
 
 
 
 --- convenient syntax:
 search [1] initSystem =>* SYSTEM:GlobalSystem such that
                            valueOf x . s in SYSTEM:GlobalSystem == [2] .
 --- also works; no solution for 2, but solution for 3
 
 
 
 *** Some temporal logic model checking:
 
 
 omod MODEL-CHECK-ADAS is
   including MODEL-CHECKER .
   including UNCLOCKED-FIG7 .
   including LF-PROP .
endom

red modelCheck(initSystem, <> [] (s in x == [3])) .
