vocabulary fischer_types
  types process,
  PcValue : Enumeration [pc_rem, pc_test, pc_set, pc_check, pc_leavetry, pc_crit, pc_reset, pc_leaveexit]
end

automaton fischer(l_check, u_set: Real) where u_set < l_check /\ u_set >= 0 /\ l_check >= 0
  imports fischer_types

  signature 
    output try(i: process)
    output crit(i: process)
    output exit(i: process)
    output rem(i: process)
    internal test(i: process)
    internal set(i: process)
    internal check(i: process)
    internal reset(i: process)

  states 
    turn: Null[process] := nil;
    pc: Array[process, PcValue] := constant(pc_rem);
    now: Real := 0;
    last_set: Array[process, AugmentedReal] := constant(\infty);
    first_check: Array[process, DiscreteReal] := constant(0);

  transitions 
    output try(i)
      pre pc[i] = pc_rem;
      eff pc[i] := pc_test;

    internal test(i)
      pre pc[i] = pc_test; 
      eff if turn = nil then
             pc[i] := pc_set;
             last_set[i] := (now + u_set);
          fi;

    internal set(i)
      pre pc[i] = pc_set;
      eff turn := embed(i);
          pc[i] := pc_check;
          last_set[i] := \infty;
          first_check[i] := now + l_check;

    internal check(i)
      pre pc[i] = pc_check /\ first_check[i] <= now;
      eff if turn = embed(i) then 
             pc[i] := pc_leavetry;
          else 
             pc[i] := pc_test;
          fi;
          first_check[i] := 0;

    output crit(i)
      pre pc[i] = pc_leavetry;
      eff pc[i] := pc_crit;

    output exit(i)
      pre pc[i] = pc_crit;
      eff pc[i] := pc_reset;

    internal reset(i)
      pre pc[i] = pc_reset;
      eff pc[i] := pc_leaveexit;
          turn := nil;

    output rem(i)
      pre pc[i] = pc_leaveexit;
      eff pc[i] := pc_rem;

  trajectories
    trajdef traj
      stop when
        \E i: process (now = last_set[i]);
      evolve
        d(now) = 1;

invariant of fischer:
  \A i: process \A j: process
     (i ~= j => (pc[i] ~= pc_crit \/ pc[j] ~= pc_crit));

invariant of fischer:
  \A i: process \A j: process
    (pc[i] = pc_leavetry \/ pc[i] = pc_crit \/ pc[i] = pc_reset
         => (turn = embed(i) /\ pc[j] ~= pc_set));

invariant of fischer:
  \A i: process (now <= last_set[i]);

invariant of fischer:
  \A i: process
     (pc[i] = pc_set => last_set[i] ~= \infty);

invariant of fischer:
  \A i: process 
     (pc[i] = pc_set => (last_set[i] <= now + u_set));


invariant of fischer:
  \A i: process \A j: process 
    (pc[i] = pc_check /\ turn = embed(i) /\ pc[j] = pc_set
         => (last_set[j] < first_check[i]));