AsmetaMA (Asmeta Model Advisor) can be used to check for common defects of AsmetaL models.
Download the tool:
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