Asmeta Model advisor

AsmetaMA (Asmeta Model Advisor) can be used to check for common defects of AsmetaL models.


Download the tool: AsmetaMA.jar

How to run

To run AsmetaMA

java -jar AsmetaMA.jar [options...] asmetalFileName.asm
 -kf    : keep the NuSMV file.
 -mp1   : No inconsistent update is ever performed
 -mp2   : Every conditional rule must be complete
 -mp3   : Every rule can eventually fire
 -mp4   : No assignment is always trivial
 -mp5   : For every domain element e there exists a location which has value e
 -mp6   : Every controlled function can take any value in its co-domain
 -mp7   : Every controlled location is updated and every location is read
 -mpAll : Execute all the metaproperties


P. Arcaini, A. Gargantini, E. Riccobene. Automatic review of Abstract State Machines by Meta Property Verification, in 2nd NASA Formal Methods Symposium (NFM 2010) link