alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* iface/dve2/README: Document state compression.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2011-06-02 19:37:20 +02:00
parent f3bae53e5b
commit 23334e7e25
2 changed files with 50 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2011-06-02 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* iface/dve2/README: Document state compression.
2011-06-02 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-06-02 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Update jQuery and jQuery-UI. Update jQuery and jQuery-UI.

46
iface/dve2/README
View file

@ -134,3 +134,49 @@ Examples
132 transitions explored 132 transitions explored
130 items max in DFS search stack 130 items max in DFS search stack
an accepting run exists (use -C to print it) an accepting run exists (use -C to print it)
Two state-compression techniques have been implemented as experiments.
Prefer the -Z option if your model use only non-negative value less
than 2^28, it is way faster than -z (which will work for all values).
Activating state compression will often reduce runtime. Compare:
% ./dve2check -T 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
122102 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
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
translating formula | 0 0.0 | 0 0.0 | 0 0.0 | 1
-------------------------------------------------------------------------------
TOTAL | 1222 100.0 | 18 100.0 | 1240 100.0 |
% ./dve2check -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
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
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
-------------------------------------------------------------------------------
TOTAL | 1051 100.0 | 10 100.0 | 1061 100.0 |
It's a 15% speedup in this case, be the improvement can be more
important on larger models.