There seems to be significant housekeeping in translated PlusCal code, especially when using procedures. Does anyone know the average cost of this housekeeping when running TLC model checker? By how much on average the state space that needs to be checked increases? How does this increase affect average running time?
-------------------------------- MODULE Func --------------------------------
EXTENDS Naturals, TLC, Sequences
Procs == 1..3
(*--algorithm Func
procedure Foo(x, y, z)
variable w;
begin
Foo1: w := x + y + z;
Foo2: return;
end procedure
process Bar \in Procs
variables a;
begin
Bar1: call Foo(1,2,3);
end process
end algorithm
*)
\* BEGIN TRANSLATION
CONSTANT defaultInitValue
VARIABLES pc, stack, x, y, z, w, a
vars == << pc, stack, x, y, z, w, a >>
ProcSet == (Procs)
Init == (* Procedure Foo *)
/\ x = [ self \in ProcSet |-> defaultInitValue]
/\ y = [ self \in ProcSet |-> defaultInitValue]
/\ z = [ self \in ProcSet |-> defaultInitValue]
/\ w = [ self \in ProcSet |-> defaultInitValue]
(* Process Bar *)
/\ a = [self \in Procs |-> defaultInitValue]
/\ stack = [self \in ProcSet |-> << >>]
/\ pc = [self \in ProcSet |-> "Bar1"]
Foo1(self) == /\ pc[self] = "Foo1"
/\ w' = [w EXCEPT ![self] = x[self] + y[self] + z[self]]
/\ pc' = [pc EXCEPT ![self] = "Foo2"]
/\ UNCHANGED << stack, x, y, z, a >>
Foo2(self) == /\ pc[self] = "Foo2"
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ w' = [w EXCEPT ![self] = Head(stack[self]).w]
/\ x' = [x EXCEPT ![self] = Head(stack[self]).x]
/\ y' = [y EXCEPT ![self] = Head(stack[self]).y]
/\ z' = [z EXCEPT ![self] = Head(stack[self]).z]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ a' = a
Foo(self) == Foo1(self) \/ Foo2(self)
Bar1(self) == /\ pc[self] = "Bar1"
/\ /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "Foo",
pc |-> "Done",
w |-> w[self],
x |-> x[self],
y |-> y[self],
z |-> z[self] ] >>
\o stack[self]]
/\ x' = [x EXCEPT ![self] = 1]
/\ y' = [y EXCEPT ![self] = 2]
/\ z' = [z EXCEPT ![self] = 3]
/\ w' = [w EXCEPT ![self] = defaultInitValue]
/\ pc' = [pc EXCEPT ![self] = "Foo1"]
/\ a' = a
Bar(self) == Bar1(self)
Next == (\E self \in ProcSet: Foo(self))
\/ (\E self \in Procs: Bar(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION