target C

reactor Controller {
  output lock: bool
  output open: bool
  output unlock: bool
  output close: bool
  physical action external: bool

  reaction(external) -> close, lock, open, unlock {=
  if (external->value == true) {
       lf_set(close, true);
       lf_set(lock, true); }
   else { lf_set(open,true);
          lf_set(unlock,true);
   }
  =}
}

reactor Door {
  input lock: bool
  input unlock: bool
  input open: bool
  input close: bool
  state locked: bool = false
  state isOpen: bool = false
  physical action extOpen: bool
  reaction(close) {=
    self -> isOpen = false; =}
  reaction(lock) {=
    if (self -> isOpen == false)
        self -> locked = true; =}
  reaction(unlock) {=
    self->locked = false; =}
  reaction(open) {=
    if (self -> locked == false)
       self -> isOpen = true; =}
  reaction(extOpen) {=
    if (self -> locked == false)
       self -> isOpen = true; =}
}

@maudePhysAct(name="external", inReactor="c", vals="true, false", period=10, timeNonDet=true)
@maudePhysAct(name="extOpen", inReactor="d", vals="true", period=11, timeNonDet=true)
//@maude(analysis="simulation", rewrites=10)
//@maude(analysis="reachability", goal="locked in d == true")
@maude(analysis="reachability", goal="(locked in d == true) /\ (isOpen in d == true)")
@maude(analysis="reachability", timeBound=150, goal="(locked in d == false) /\ (d.2 invoked)")
//@maude(analysis="ltl", goal="<>(locked in d == true)")
//@maude(analysis="ltl", goal="(((~ (event(c, external, false) inQueue)) W (locked in d == true))) /\ ([] (<> (event(c, external, true) inQueue))) -> <>(locked in d == true)")
@maude(analysis="ltl", goal="<> ((locked in d == false) /\ ((d.2) invoked))")

main reactor {
  c = new Controller()
  d = new Door()
  c.lock -> d.lock after 5 msec
  c.unlock -> d.unlock after 4 msec
  c.open -> d.open after 7 msec
  c.close -> d.close after 3 msec
}
