Skip to content
GitLab
Commit c524f32d authored by Etienne Renault's avatar Etienne Renault
Browse files

modelcheck: update output and documentation 

Fixes #330.

* tests/ltsmin/README,
tests/ltsmin/modelcheck.cc: here.
parent f786a2df
Hide whitespace changes
Inline Side-by-side
tests/ltsmin/README
View file @ c524f32d
......@@ -144,31 +144,34 @@ Examples
that the critical section is accessed infinitely often by some
processes using:
% ./modelcheck beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
% ./modelcheck --model beem-peterson.4.dve --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --is-empty
2239039 unique states visited
0 strongly connected components in search stack
11449204 transitions explored
1024245 items max in DFS search stack
111081 pages allocated for emptiness check
no accepting run found
Process P_0 can starve, waiting to enter in critical section:
% ./modelcheck beem-peterson.4.dve '!G(P_0.wait -> F P_0.CS)'
2190 unique states visited
34 strongly connected components in search stack
4896 transitions explored
83 items max in DFS search stack
an accepting run exists (use -C to print it)
% ./modelcheck --model beem-peterson.4.dve --formula '!G(P_0.wait -> F P_0.CS)' --is-empty
3978 unique states visited
31 strongly connected components in search stack
4723 transitions explored
3302 items max in DFS search stack
1099 pages allocated for emptiness check
an accepting run exists (use -c to print it)
Variable pos[1] is not always < 3 (this formula makes no sense, it
is just to demonstrate the use of double quote).
% ./modelcheck beem-peterson.4.dve '!G("pos[1] < 3")'
% ./modelcheck --model beem-peterson.4.dve --formula '!G("pos[1] < 3")' --is-empty
130 unique states visited
61 strongly connected components in search stack
132 transitions explored
130 items max in DFS search stack
an accepting run exists (use -C to print it)
512 pages allocated for emptiness check
an accepting run exists (use -c to print it)
Two state-compression techniques have been implemented as experiments.
......@@ -177,41 +180,102 @@ than 2^28, it is way faster than -z (which will work for all values).
Activating state compression will often reduce runtime. Compare:
% ./modelcheck -T beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
$ ./modelcheck --model beem-peterson.4.dve --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --is-empty --timer
2239039 unique states visited
0 strongly connected components in search stack
11449204 transitions explored
1024245 items max in DFS search stack
122102 pages allocated for emptiness check
no accepting run found
| user time | sys. time | total |
111081 pages allocated for emptiness check
no accepting run found | user time | sys. time | total |
name | ticks % | ticks % | ticks % | n
-------------------------------------------------------------------------------
loading dve2 | 0 0.0 | 0 0.0 | 0 0.0 | 1
loading ltsmin model | 0 0.0 | 0 0.0 | 0 0.0 | 1
parsing formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
reducing A_f w/ SCC | 0 0.0 | 0 0.0 | 0 0.0 | 1
running emptiness chec | 1222 100.0 | 18 100.0 | 1240 100.0 | 1
running emptiness chec | 672 100.0 | 13 100.0 | 685 100.0 | 1
translating formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
-------------------------------------------------------------------------------
TOTAL | 1222 100.0 | 18 100.0 | 1240 100.0 |
TOTAL | 672 100.0 | 13 100.0 | 685 100.0 |
$ ./modelcheck --model beem-peterson.4.dve --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --is-empty --timer -z 2
% ./modelcheck -T -Z beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
2239039 unique states visited
0 strongly connected components in search stack
11449204 transitions explored
1024245 items max in DFS search stack
78580 pages allocated for emptiness check
85991 pages allocated for emptiness check
no accepting run found
| user time | sys. time | total |
| user time | sys. time | total |
name | ticks % | ticks % | ticks % | n
-------------------------------------------------------------------------------
loading dve2 | 0 0.0 | 0 0.0 | 0 0.0 | 1
loading ltsmin model | 40 6.1 | 2 16.7 | 42 6.2 | 1
parsing formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
reducing A_f w/ SCC | 0 0.0 | 0 0.0 | 0 0.0 | 1
running emptiness chec | 1051 100.0 | 10 100.0 | 1061 100.0 | 1
translating formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
running emptiness chec | 620 93.8 | 10 83.3 | 630 93.6 | 1
translating formula | 1 0.2 | 0 0.0 | 1 0.1 | 1
-------------------------------------------------------------------------------
TOTAL | 1051 100.0 | 10 100.0 | 1061 100.0 |
TOTAL | 661 100.0 | 12 100.0 | 673 100.0 |
It's a 15% speedup in this case, be the improvement can be more
It's a 14% speedup in this case, be the improvement can be more
important on larger models.
The parallel deadlock detection has also been implemented is this tool:
% ./modelcheck --model beem-peterson.4.dve --has-deadlock --csv -p 1
Thread #0: on CPU 0
---- Thread number : 0
1119560 unique states visited
3864896 transitions explored
78157 items max in DFS search stack
1316 milliseconds
Find following the csv: thread_id,walltimems,type,states,transitions
@th_0,1316,NO-DEADLOCK,1119560,3864896
Summary :
No no deadlock found!
Find following the csv: model,walltimems,memused,type,states,transitions
#beem-peterson.4.dve,1317,103681,NO-DEADLOCK,1119560,3864896
Running the same algorithm with 3 threads save 40% of the computation time:
$ ./modelcheck --model beem-peterson.4.dve --has-deadlock --csv -p 3
Thread #1: on CPU 1
Thread #2: on CPU 2
Thread #0: on CPU 0
---- Thread number : 0
417923 unique states visited
1418775 transitions explored
56403 items max in DFS search stack
819 milliseconds
Find following the csv: thread_id,walltimems,type,states,transitions
@th_0,819,NO-DEADLOCK,417923,1418775
---- Thread number : 1
526175 unique states visited
1813440 transitions explored
69322 items max in DFS search stack
819 milliseconds
Find following the csv: thread_id,walltimems,type,states,transitions
@th_1,819,NO-DEADLOCK,526175,1813440
---- Thread number : 2
404501 unique states visited
1411645 transitions explored
61888 items max in DFS search stack
819 milliseconds
Find following the csv: thread_id,walltimems,type,states,transitions
@th_2,819,NO-DEADLOCK,404501,1411645
Summary :
No no deadlock found!
Find following the csv: model,walltimems,memused,type,states,transitions
#beem-peterson.4.dve,820,158211,NO-DEADLOCK,404501,1411645
One can observe that when possible (i.e., if the OS allows it) we try
has much as possible to pin threads to a CPU.
tests/ltsmin/modelcheck.cc
View file @ c524f32d
......@@ -340,7 +340,7 @@ static int checked_main()
if (!res)
{
std::cout << "no accepting run found";
std::cout << "no accepting run found" << std::endl;
}
else if (!mc_options.compute_counterexample)
{
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment