00_OutSanyParser.tla

--------------------------- MODULE 00_OutSanyParser ---------------------------

EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache

(*
  @type: ((Set(a), a) => Set(a));
*)
add(s, e) == s \union {e}

(*
  @type: (() => Int);
*)
t_min == 0

(*
  @type: (() => Int);
*)
t_max == 5

(*
  @type: ((Int) => { id: Int });
*)
Proc(id) == [id |-> id]

(*
  @type: ((b, c) => { src: b, ts: c });
*)
msgFrom(p, ts) == [src |-> p, ts |-> ts]

VARIABLE
  (*
    @type: Int;
  *)
  time

VARIABLE
  (*
    @type: ({ id: Int } -> Int);
  *)
  hc

VARIABLE
  (*
    @type: Set({ src: { id: Int }, ts: Int });
  *)
  msgs

VARIABLE
  (*
    @type: ({ id: Int } -> Set({ src: { id: Int }, ts: Int }));
  *)
  rcvd

VARIABLE
  (*
    @type: ({ id: Int } -> Str);
  *)
  state

(*
  @type: (() => Set(Str));
*)
states == { "init", "sent", "sync" }

(*
  @type: Bool;
*)
ASSUME(t_min >= 0 /\ t_max > t_min)

(*
  @type: (() => Set({ id: Int }));
*)
Procs == { (Proc(1)), (Proc(2)) }

(*
  @type: (({ id: Int }) => Bool);
*)
sendMsg(p) ==
  state[p] = "init"
    /\ msgs' := (add(msgs, (msgFrom(p, hc[p]))))
    /\ state' := [ state EXCEPT ![p] = "sent" ]
    /\ rcvd' := rcvd

(*
  @type: (({ id: Int }) => Bool);
*)
receiveMsg(p) ==
  \E newMsg \in msgs:
    ~(newMsg \in rcvd[p])
      /\ hc[newMsg["src"]] >= newMsg["ts"] + t_min
      /\ rcvd' := [ rcvd EXCEPT ![p] = add(rcvd[p], newMsg) ]
      /\ state' := state
      /\ msgs' := msgs

(*
  @type: (() => Bool);
*)
init ==
  (\E time0 \in Nat: time' := time0)
    /\ (\E hc0 \in [(Procs) -> Nat]: hc' := hc0)
    /\ msgs' := {}
    /\ state' := [ __QUINT_UNDERSCORE_403 \in Procs |-> "init" ]
    /\ rcvd' := [ __QUINT_UNDERSCORE_410 \in Procs |-> {} ]

(*
  @type: ((Int) => Bool);
*)
advanceClocks(delta) ==
  delta > 0
    /\ (\A m \in msgs:
      hc[m["src"]] + delta > t_max => (\A p \in Procs: m \in rcvd[p]))
    /\ time' := (time + delta)
    /\ hc' := [ p \in Procs |-> hc[p] + delta ]

(*
  @type: (() => Bool);
*)
step ==
  (msgs' := msgs
      /\ state' := state
      /\ rcvd' := rcvd
      /\ (\E delta \in Int: advanceClocks(delta)))
    \/ (time' := time
      /\ hc' := hc
      /\ (\E p \in Procs: sendMsg(p) \/ receiveMsg(p)))

================================================================================