search

utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
52 stars 30 forks source link

bug in mu-calculus / parity-game solver #90

Closed jacopol closed 7 years ago

jacopol commented 7 years ago

The formula nu Z1. []Z1 && ["r1(d1)"] mu Z3. <"s4(d1)">true || []Z3 should be false on abp.lps, but we get:

etf2lts-sym --mucalc complex2.mucalc abp.etf --pg-write=abp_complex2.spg spgsolver abp_complex2.spg ...The result is: true...

(in ltsmin 3.0, osx-clang compiled version)

This can be checked in mcrl2 on the following corresponding formula: nu Z1. [true]Z1 && [r1(d1)] mu Z3. <s4(d1)>true || [true]Z3

lps2pbes abp.lps -f complex2.mucrl abp2.pbes pbes2bool abp2.pbes ...false...

gijskant commented 7 years ago

The bug does not seem to be in the parity game solver (that also is used when verifying the PBES with pbes2lts-sym --pg-solve), but in either the formula parser or the mucalc layer. I am looking into it.

jacopol commented 7 years ago

It seems to go wrong already with this formula: <"r1(d1)">true

Should be true (for abp) but is deemed false. Hope this simpler formula helps solving the problem

gijskant commented 7 years ago

The mucalc layer receives action labels like MultAct([Action(ActId(r1,[SortId(D)]),[OpId(d1,SortId(D),80)])]). Apparently something goes wrong with pretty printing of the action labels when using the mucalc layer. And there was a bug in the initialisation of action labels in the mucalc layer.

gijskant commented 7 years ago

Actually, these internal labels were caused by a flag I used for testing. So, it's only the initialisation, which is now fixed. Pull request is on its way.

Meijuh commented 7 years ago

@jaco @gijs is this fixed in the current next branch? Can I close this issue?

gijskant commented 7 years ago

@Meijuh Yes, the changes of #91 have been applied to next, fixing the issue.