|
Before installing the Crocodile plugin, you must have Eclipse along with the Coloane plugin installed.
To install Coloane, please follow these instructions.
Then, to install the GML export par of Crocodile, proceed as follows:
- Launch your Eclipse application as usual.
- In Help menu, choose Install new software.
- In the Work with text field, type in "http://coloane.lip6.fr/night-updates".
- Eclipse will now look for the newest version of Coloane and its extensions.
- Choose Import/Export Wizards, then check ExportToGML.
- Click on button Next.
- A recap window appears. Click Next.
- You now must agree the terms of the licence. Click then on button Finish.
- Eclipse will now install the plugin and any possible required dependencies.
- You then have to restart Eclipse as asked in order for the installation to take effect.
Open the Coloane perspective in Eclipse, and draw a SNB.
Then, in the menu Coloane Services, in the submenu Local Tools, choose Crocodile SRG Generator.
Eclipse will feed your model to Crocodile and run it.
The result appear in the console.
The integration into Eclipse might not be very convenient when running experiments on various models.
You can get the command-line tool Crocodile here (log as a guest).
In the Crocodile section, choose the executable corresponding to your configuration (so far, Linux 32 or 64 bits, MacOS 10.6 32+64 bits, and Windows 32 bits).
All these version have not been tested extensively, so architecture-related problems may occur.
Do not hesitate to report them !
Crocodile is basically a Symbolic Reachability Graph (SRG) generator, that counts the number of symbolic states in this SRG.
It has been extended to check reachability formulae.
Crocodile as a command-line tool takes one or two arguments.
The first one must be a SNB given in the gml format. Coloane provides an exporter to this format, that is installed when the Crocodile Eclipse plug-in is installed.
The second (optional) file is a file of reachability formulae.
Their syntax is described here.
|
