***  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:

in lf-representation

omod FIG7 is

 including LF-REPR .


 op s : -> IVarId [ctor] .
 ops relay x y : -> ReactorId [ctor] .
 ops inc dbl r out : -> IPortId [ctor] .
 op startup : -> IActionId .
 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


in dynamics.maude

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:

in model-checker.maude


omod MODEL-CHECK-ADAS is
  including MODEL-CHECKER .
  including UNCLOCKED-FIG7 .
  subsort ClockedSystem < State .

  --- generic atomic proposition:

  var REST : Configuration .
  var REACTORID : ReactorId .
  var VAR : VarId .
  var VAL : Value .
  var RS : ReactorState .
  var T : Time .
  var O : Oid .

  vars EQ1 EQ2 : EQueue .
  var EVENT : Event .
  var TAG : Tag .

  op _in_is_ : VarId ReactorId Value -> Prop [ctor] .

  eq {REST
      < REACTORID : Reactor | state : (VAR |-> VAL) ; RS >}
     |= VAR in REACTORID is VAL = true . 

  eq {REST
      < REACTORID : Reactor | state : (VAR |-> VAL) ; RS >} in time T
     |= VAR in REACTORID is VAL = true .


  --- An event is in the event queue:
  op _isInQueue : Event -> Prop [ctor] .

  eq {REST
      < O : EventQueue | queue : (EQ1 :: (EVENT at TAG) :: EQ2) >}
     |=  EVENT isInQueue = true .

  eq {REST
      < O : EventQueue | queue : (EQ1 :: (EVENT at TAG) :: EQ2) >} in time T
     |=  EVENT isInQueue = true .

endom

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