modelcheck with and without compression gives different answers
ltsmin/modelcheck: emptiness check gives different answers while using this kind of compression should never impact the result...
./ltsmin/modelcheck -e telephony.2.dve 'XF"User_0.error_state" <-> ("User_0.busy" -> ("User_0.dialing" & "User_1.error_state"))'
51827 unique states visited
0 strongly connected components in search stack
200325 transitions explored
23529 items max in DFS search stack
0 pages allocated for emptiness check
no accepting run found
./ltsmin/modelcheck -z -e telephony.2.dve 'XF"User_0.error_state" <-> ("User_0.busy" -> ("User_0.dialing" & "User_1.error_state"))'
1322 unique states visited
10 strongly connected components in search stack
4678 transitions explored
1117 items max in DFS search stack
0 pages allocated for emptiness check
an accepting run exists (use -C to print it)