| Hi Markus, ProB also uses DOT to render the state space, this puts a severe limit on how much states and transitions can be rendered within reasonable time (and how much this information is of use to users). When you exceed about 100 transitions the rendering time starts becoming very high, if I remember correctly. The ProB tool displays a warning when the state space exceeds 250 nodes, asking the user to confirm whether dot should be launched. What I find very useful, however, is the state space projection feature: basically, the user types an _expression_ and ProB evaluates the _expression_ over the state space and displays the projected graph. Below is an example for a TLA hour-minute-seconds clock. The state space is too large to render with DOT, however, one can type in an _expression_ like “hour” and obtain the projection. The graph is attached below, dotted lines mean that the action is not always possible or does not always lead to the target equivalence class. A solid line means the action is always possible and always leads to the same equivalence class. This graph actually shows that the hour progression (0 -> 1 -> 2….) is correct, but also highlights a bug in the model: if the hour is 1..11, then the next state always increases the hour by one. (I leave the task of correcting the model to the interested reader). (I don’t know where the model is from; while typing this post I was looking for a TLA+ model to showcase the projection diagram and didn’t expect the model to be faulty ;-)). I also attach another example below: the Sieve Prime number algorithm, with MAX=1000 and where the state space is projected onto s=Cardinality(N). Other (B) examples, such as the ABZ’14 landing gear, are in an ICFEM’2015 paper, in case you are interested.
Kind regards, Michael ---------------------- MODULE clock_init0 ---------------------- EXTENDS Naturals VARIABLES hours, minutes, seconds Init == hours = 0 /\ minutes = 0 /\ seconds = 0 Next == hours' = (IF minutes # 59 THEN hours ELSE (hours + 1) % 12) /\ minutes' = (IF seconds # 59 THEN minutes ELSE (minutes + 1) % 60) /\ seconds' = (seconds + 1) % 60 Clock == Init /\ [][Next]_{seconds} -------------------------------------------------------------- THEOREM Hansen ============================================================== ---- MODULE Sieve_Full ---- EXTENDS Naturals, FiniteSets CONSTANT MAX VARIABLE cur, N, s Init == /\ cur = 2 /\ N = 2..MAX /\ s = Cardinality(N) prime == /\ cur \in N /\ cur' = cur+1 /\ N' = N \ {cur*n : n\in cur..(MAX \div cur) } /\ s' = Cardinality(N') nprime == /\ cur \notin N /\ cur*cur < MAX /\ cur' = cur+1 /\ UNCHANGED <<N,s>> Next == prime \/ nprime Spec == Init /\ [] [Next]_<<cur,N,s>> =================== |
Attachment:
clock_init0_hour_projection.pdf
Description: Adobe PDF document
Attachment:
Sieve_Full_projection_s.pdf
Description: Adobe PDF document