target C {
    timeout: 10 msec
}

reactor _Factorial {
    output out:int
    timer t(0, 1 msec);
    logical action prepForNext

    state N:int = 0
    state result:int
    state lastResult:int

    reaction(t) -> out, prepForNext {=
        if (self->N < 2) {
            self->result = 1;
        } else {
            self->result = self->N * self->lastResult;
        }
        lf_set(out, self->result);
        lf_schedule(prepForNext, 0);
    =}
    reaction(prepForNext) {=
        self->N += 1;
        self->lastResult = self->result;
    =}
}

reactor Printer {
    input in:int
    state result:int
    reaction(in) {=
        self->result = in->value;
        printf("%d\n", self->result);
    =}
}

//@property(name="correctness", tactic="bmc", spec="G[10 msec](Factorial_printer_reaction_0 ==> Factorial_printer_result == 3628800)", expect=true)
@maude(analysis="reachability", timeBound=10, goal="(printer.1 invoked) /\ (result in printer != 3628800) /\ remainingTime 0")
main reactor {
    factorial = new _Factorial()
    printer = new Printer()
    factorial.out -> printer.in
}
