Lustre Plug-in for Eclipse with JKind Analysis Support
This plug-in provides a Lustre front-end in Eclipse with syntax checking, highlighting, type checking, and other syntatic checks. The plug-in also provides a convenient way to launch JKind on a Lustre file and have the results reported back in a real-time graphical display. Excel formatted counterexamples are viewable by right-clicking on individual properties.
JKind itself is now bundled into the plug-in, so no separate installation is needed.
Use the update site https://raw.githubusercontent.com/agacek/jkind-xtext/master/jkind.xtext.site/site.xml
-
Download and install Eclipse.
-
From the Eclipse "Help" menu select "Install New Software...".
- In the "Available Software" dialog click the "Add..." button.
- In the "Add Repository" dialog enter the name
JKind-Xtextand the locationhttps://raw.githubusercontent.com/agacek/jkind-xtext/master/jkind.xtext.site/site.xml. Click "OK".
- In the "Available Software" dialog open the "Uncategorized" menu and select "JKind for Eclipse". Click "Next" and follow the prompts.
To update the plug-in, select "Check for Updates" from the Eclipse "Help" menu.
Right click in a Lustre file to run JKind and examine the results:
Syntax checking, type checking, and other static checks are all done on the fly:
Many other Eclipse-style features are available. For example, variables and fields can be easily renamed:
