target C  {
    timeout: 10 msec
  }

reactor Fib {
  output out:int
  timer t(0, 1 msec);
  logical action incrementN
  logical action saveLast
  logical action saveSecondLast
  state N:int = 0
  state result:int = 0
  state lastResult:int = 0
  state secondLastResult:int = 0
  reaction(t) -> out, incrementN, saveLast, saveSecondLast {=
    if (self->N < 2) {
      self->result=1;
    } else {
      self->result = self->lastResult + self->secondLastResult; }
    lf_set(out,self->result);
    lf_schedule(incrementN,0);
    lf_schedule(saveLast,0);
    lf_schedule(saveSecondLast,0);   
  =}
  reaction(incrementN) {=
    self->N += 1;       =}
  reaction(saveSecondLast) {=
    self->secondLastResult=self->lastResult; =}
  reaction(saveLast) {=
self->lastResult = self->result; =}
}
reactor Printer {
  input in:int
  state result:int
  reaction(in) {=
    self->result = in->value;  =}
}

//@maude(analysis="simulation", timeBound=10)
//@maude(analysis="reachability", timeBound=10, goal="False")
//@maude(analysis="reachability", timeBound=10, goal="result in printer == 89", type="!")
//@property(name="correctness", tactic="bmc", spec="G[10 msec](Fibonacci_printer_reaction_0 ==> Fibonacci_printer_result == 89)", expect=true)
@maude(analysis="reachability", timeBound=10, goal="(printer.1 invoked) /\ (result in printer != 89) /\ remainingTime 0" )

main reactor {
  fib = new Fib()
  printer = new Printer()
  fib.out -> printer.in
}
