Asmeta Model checker

The AsmetaSMV model checker can be used to automatically verify Asmeta properties by translating AsmetaL specifications in NuSMV specifications.

The AsmetaSMV can be used either emebedded as a plugin in asmee or as standalone program.

Download

Download the tool: AsmetaSMV.jar

How to run

To run AsmetaSMV

java -jar AsmetaSMV.jar [options...] file.asm
 -debug   : set log4j level to debug
 -en      : execute the NuSMV model after the mapping
 -kf      : keep the NuSMV file. To be used with the -en option enabled. If the -en option is not enabled, the option -kf is enabled by default.
 -log VAL : log4j configuration file
 -nc      : do not add the check on integer enum
 -ns      : do not simplify the boolean conditions in NuSMV code

Eclipse plugin

The tool is also available as eclipse plugin at this update site http://svn.code.sf.net/p/asmeta/code/code/stable/asmeta_update/

You can run the tool in two modes:

  • translates the AsmetaL model in NuSMV
  • translates the AsmetaL model in NuSMV and then executes the NuSMV model

Other options can be set in the preferences: Window -> Preferences -> Asmeta -> AsmetaSMV