To upgrade JTLV:
-
Open eclipse.
-
Open and right click every JTLV project that you have in
your workspace, and un-toggle the "JTLV X.X.X
Nature".
-
Close eclipse.
-
Delete JTLV jar file at {eclipse installation
folder}/plugins/JTLV_X.X.X.jar, and replace it with
the new JTLV jar file.
-
Open eclipse.
-
Open and right click every JTLV project that you have in
your workspace, and toggle back JTLV's nature. (it
will make sense to toggle and un-toggle few times,
to make sure that the new jar file is loaded.)
-
Follow the errors in case the API has changed in
the new release. (usually, we are not deleting
functionality, in the worst case we are just
renaming it, or change its package)
** These instructions are on safe side. Theoretically it
would be enough to replace the previous jar with the new
JTLV jar, restart eclipse, and toggle the nature few times.
|
To get you started with JTLV here are few basic HOWTOs:
-
Open eclipse and choose a workspace (i.e. a folder
you wish to work in).
-
Open a new JTLV project (1):
-
Go to "File" -> "New" -> "Other".
-
Select "JTLV Project" and click "Next".
-
Follow the wizard till clicking "Finish".
-
Open a new JTLV project (2):
-
Go to "File" -> "New" -> "Other".
-
Select "Java Project" and click "Next".
-
Follow the wizard till clicking "Finish".
-
Right click the newly created Java project at
the "Package Explore" Pane.
-
Click the "Toggle JTLV X.X.X Nature".
-
Create a new SMV or SPC file (1):
-
Go to "File" -> "New" -> "File".
-
Name the file with a "smv" or "spc" extension, and
Follow the wizard till clicking "Finish".
-
Start editing your SMV or SPC file.
-
Create a new SMV or SPC file (2):
-
Go to "File" -> "New" -> "Other".
-
Select "SMV File" or "SPC File", and click "Next".
-
Follow the wizard till clicking "Finish".
-
Start editing your SMV or SPC file.
-
If you are not familiar with Java, then start with
a simple Main Class.
To start your Java application:
-
Go to "File" -> "New" -> "Class".
-
Mark the "public static void main(String[]
args)", and follow the wizard till clicking
"Finish".
-
A new Java file with a main procedure
will be created, just start editing your
application.
-
Executing and debugging:
-
To execute your application, open it, and
click at the "play" button at
the top left side of eclipse window.
-
To debug your application, open it, click
on the thin left column just to the left of
your Java editing pane, at the line you wise to
set a breakpoint. Click at the "bug" button at
the top left side of eclipse window. When
the execution will encounter a breakpoint,
eclipse will offer you to change to
debugging perspective. At the debugging perspective
you will see a new set of buttons and windows to
debug your application. To return to the
Java editing perspective, click the "perspective
chooser" at the top right side of eclipse window.
-
Load SMV files into your application by:
|
// ...
|
|
// path to your smv file in your project.
|
|
String filename =
"./arbiter.smv" ;
|
|
Env.loadModule(filename);
|
|
// path to the exact module in the smv
file.
|
|
String module_name =
"main.P1" ;
|
|
Module m = Env.getModule(module_name);
|
|
// Now you can start performing
basic operation on object "m",
|
|
// such as ".initial()" to get the
initial states, etc.
|
|
// ** for more basic functionalities,
the user can consult the javadocs
|
At the first time, you'll see an error
since you did not import "Env", and
"Module" objects. Just click the light
bult error marker at the left side of
the editing pane, and eclipse will suggest
to import "Env" from JTLV's library. Click
eclipse suggestion, and an import statement
will be added to the top of your file.
-
Load specifications, into your application by:
|
// ...
|
|
// path to your spc file in your project.
|
|
String filename =
"./arbiter.spc" ;
|
|
Spec[] sp = Env.loadSpecFile(filename);
|
|
// Or,
|
|
String spc_str =
"LTLSPEC <>[]P1.x; \n"
;
|
|
spc_str +=
"LTLSPEC P1.x U P2.y; \n";
|
|
spc_str +=
"CTLSPEC EF(P1.x); \n"
;
|
|
spc_str +=
"CTL*SPEC EF(([]<>P1.x) U ([]<>P2.y)); \n"
;
|
|
Spec[] sp2 = Env.loadSpecString(spc_str);
|
|
|
|
// Now you can start addressing
the specifications array.
|
|
// For instance if sp contains at
least a single specification then
|
|
// "sp[0].isLTLSpec()" will return
whether it is a LTL specification.
|
|
// ** for more basic functionalities,
the user can consult the javadocs
|
Again, at the first time, you'll see an error
since you did not import "Env", and
"Spec" objects. Just click the light
bult error marker at the left side of
the editing pane, and eclipse will suggest
to import "Env" from JTLV's library. Click
eclipse suggestion, and an import statement
will be added to the top of your file.
|