Piotr Szwed

**This is an old revision of the document!** ----

===== Archimate to NuSMV (nuXmv) ===== //Archimate to NuSMV// is a plugin to popular [[http://www.archimatetool.com/|Archi editor]]. The plugin examines business processes embeded within the Business layer and builds a model suitable for model checking with NuSMV or nuXmv. ==== General description ==== ==== Installation ==== Following the instructions in: [[http://www.archimatetool.com/dev/import-export]] - Download the [[http://pszwed.kis.agh.edu.pl/code/2015/archi/pl.edu.agh.kis.pszwed.archi.nusmvexport_1.0.0.201605202317.jar|compiled plugin (JAR)]] controlling the model generation - Copy it to the //plugins// directory of Archi installation - Restart Archi - A new menu item //File//->//Export//->//Model to NuSMV// should appear. ==== Controlling model generation ==== Model genetration is controlled by the properties file named ''NuSMVExport.properties''. The file should be placed in a location depending on the platform. However, when you use Archi to NuSMV option for the first time, the plugin reports missing properties file and creates it in a recommended location. User is notified of the file creation with a message box similar to the one below. {{:archi_to_nusmv-properties.png?300|Notification on creation default properties file (Windows platform)}} *Please take a note, where the ''NuSMVExport.properties'' was created, in the case you wish to edit it. *Downolad example properties file [[http://pszwed.kis.agh.edu.pl/code/2015/archi/NuSMVExport.properties|NuSMVExport.properties]] <code> specification.generate=true # generate CTL specification specification.generate.ctl.universal specification.generate.ctl.existential=true specification.generate.reachable.or=true specification.generate.reachable.and=true specification.generate.module=false #generate specification for modules # For the below elements there is a choice between synchronous and interleaving implementation # interleaving implementation: FSM model is used for a given element, i.e. there are intermediary states between an input occurrence and output # synchronous: output is generated synchronously with the input semantcis.event=synchronous semantcis.process=interleaving #semantcis.process=synchronous semantcis.xorfork=synchronous semantcis.xorjoin=synchronous semantcis.andfork=synchronous semantcis.andjoin=synchronous #semantcis.event=interleaving #semantcis.process=interleaving #semantcis.xorfork=interleaving #semantcis.xorjoin=interleaving #semantcis.andfork=interleaving #semantcis.andjoin=interleaving refactoring.remove.process=false #a process with one input and one output can be removed </code>