Sir,
I m a beginner in TLA+ and my research area is Formal method .While i
m writing a spec in TLA+ , there occurs execution errors. I couldn't
rectify those errors pls correct it. I m attaching the spec also in
PDF
EXTENDS Integers
VARIABLES i,pc,j
Init == (pc="start") /\ (i=0) /\ (j=2)
Pick == \/ /\ pc="start"
/\ i' \in 0..1000
/\ j' \in 2..1002
/\ i = IF i>j THEN i ELSE j
/\ pc'="middle"
Max == \/ /\ pc="middle"
/\ i' = IF i > j THEN i ELSE j
/\ pc'="done"
Next == Pick \/ Max
Regards
renjith S
Dept of CSE
Amrita sChool of Engg
Attachment:
maxof2.tex
Description: Binary data