diff --git a/coloane/fr.lip6.move.coloane.projects.its/.project b/coloane/fr.lip6.move.coloane.projects.its/.project
index e922e0343d..b9640afe3b 100644
--- a/coloane/fr.lip6.move.coloane.projects.its/.project
+++ b/coloane/fr.lip6.move.coloane.projects.its/.project
@@ -35,8 +35,14 @@
+
+ org.eclipse.m2e.core.maven2Builder
+
+
+
+ org.eclipse.m2e.core.maven2Nature
org.maven.ide.eclipse.maven2Nature
org.eclipse.pde.PluginNature
org.eclipse.jdt.core.javanature
diff --git a/coloane/fr.lip6.move.coloane.projects.its/.settings/org.eclipse.m2e.core.prefs b/coloane/fr.lip6.move.coloane.projects.its/.settings/org.eclipse.m2e.core.prefs
new file mode 100644
index 0000000000..f897a7f1cb
--- /dev/null
+++ b/coloane/fr.lip6.move.coloane.projects.its/.settings/org.eclipse.m2e.core.prefs
@@ -0,0 +1,4 @@
+activeProfiles=
+eclipse.preferences.version=1
+resolveWorkspaceProjects=true
+version=1
diff --git a/fr.lip6.move.gal.updatesite/category.xml b/fr.lip6.move.gal.updatesite/category.xml
index 868c1b1702..5a19639d28 100644
--- a/fr.lip6.move.gal.updatesite/category.xml
+++ b/fr.lip6.move.gal.updatesite/category.xml
@@ -1,57 +1,57 @@
-
-
-
- GAL Incubation Updates Site
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- This category provides a single click install path for the full ITS modeler environment.
-
-
-
-
- Provides various functionalities of the ITS-modeler environment as separate packages : choose which of these are relevant for your use case.
-
-
-
-
- This category groups plugins tagged as "work in progress".
-
-
-
+
+
+
+ GAL Incubation Updates Site
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ This category provides a single click install path for the full ITS modeler environment.
+
+
+
+
+ Provides various functionalities of the ITS-modeler environment as separate packages : choose which of these are relevant for your use case.
+
+
+
+
+ This category groups plugins tagged as "work in progress".
+
+
+
diff --git a/itstools/doc.md b/itstools/doc.md
new file mode 100644
index 0000000000..a90276d714
--- /dev/null
+++ b/itstools/doc.md
@@ -0,0 +1,113 @@
+---
+title: Configuration and Running of GAL-model files with the ITS_Tools
+---
+
+How to configure and run GAL model files with ITS_Tools?
+=================================================
+
+This documentation aims to give you an interactive way to configure and run GAL mode files using ITS_Tools in an eclipse configuration window. Several options have been chosen among all those available in the command-line its-tools version.
+They are:
++ Input options (mandatory):
+----------------------------
+
+ -i path : specifies the path to the input model file.
+
+ -t {CAMI|PROD|ROMEO|ITSXML|ETF|DVE|GAL|DLL|NDLL} : specifies format of the input model file :
+
+ CAMI : CAMI format (for P/T nets) is the native Petri net format of CPN-AMI
+ PROD : PROD format (for P/T nets) is the native format of PROD
+ ROMEO : an XML format (for Time Petri nets) that is the native format of Romeo
+ ITSXML : a native XML format (for ANY kind of ITS) for this tool. These files allow to point to other files and are used as main file for composite definitions. See this example, the list of formalism/format supported is described here.
+ ETF : Extended Table Format is the native format used by LTSmin, built from many front-ends.
+ DVE : Divine is a modelling language similar to Promela. Input file should be in Divine format.
+ GAL : Guarded Action Language. Input file should be in GAL syntax.
+ DLL : use a dynamic library that provides a function "void loadModel (Model &,int)" typically written using the manipulation APIs. See demo/ folder.
+ NDLL : same as DLL, but expect input formatted as size:lib.so. See demo/ folder for a usage example. Both DLL and NDLL are used to inject of arbitrary C++ ITS types into the ITSModel.
+
+
++ An option related to Variable Order:
+------------------------------------
+
+ --dump-order path : dump the currently used variable order to file designated by path and exit.
+
+ + Options related to Encoding of ITS types
+ -------------------------------------------
+
+ For Petri nets, there is a choice between an SDD encoding, where to each variable is associated the set of integer values it can take, or a DDD encoding, where each edge of the decision diagram is labeled by a single value (i.e. like MDD). The default used is the SDD encoding, but option --ddd sometimes works better when markings (or transition latest firing times) have large values.
+
+ --sdd : privilege SDD storage (Petri net models only).[DEFAULT]
+ --ddd : privilege DDD (no hierarchy) encoding (Petri net models only).
+
+ For Scalar and Circular symmetric composite types, the following options allow to use recursive state encodings. The default setting is "-ssD2 1", i.e. for a Scalar or Circular set of size n, define n SDD variables, one per subcomponent.
+
+ -ssD2 INT :[DEFAULT: -ssD2 1] (depth 2 levels) use 2 level depth for scalar sets. Integer provided defines level 2 block size.
+ -ssDR INT : (depth recursive) use recursive encoding for scalar sets. Integer provided defines number of blocks at highest levels.
+ -ssDS INT : (depth shallow recursive) use alternative recursive encoding for scalar sets. Integer provided defines number of blocks at lowest level.
+
+
++ Options related to gc policy
+-------------------------------
+
+ Garbage collection options :
+ --no-garbage : disable garbage collection (may be faster, more memory)
+ --gc-threshold INT : set the threshold for first starting to do gc [DEFAULT:13000 kB=1.3GB]
+
+ + Options related to saturation
+ --------------------------------
+
+ Two variants of saturation are possible, controlling how clusters are applied at a given level. The BFS variant chains application of each transition cluster using a round robin, while the DFS variant chains applications to a fixpoint of each cluster. The DFS variant can be very efficient when a given transition cluster can be fired several times in a row. This could be the case for a transition with a high level of non-determinism, or a transition such as "time elapses" which can often be chained without firing other transitions. Petri nets with large marking values also often exhibit this behavior where a transition can be fired several times in a row.
+
+ The default setting is BFS, except if loading Time Petri nets where the default becomes DFS (more efficient in our experiments). Manually setting the strategy overrules these defaults.
+
+ --fixpoint {BFS,DFS} : this options controls which kind of saturation algorithm is applied. Both are variants of saturation not really full DFS or BFS. [default: BFS]
+
+
++ An Option controlling the reachable set computation ( specific to its-reach)
+
+ The default behavior of its-reach is to build the full state space (which is hopefully finite), using saturation. This behavior can be changed to force a bounded BFS exploration (i.e. bounded model-checking or bmc) of the state space over a given number of steps.
+
+ -bmc XXX : use limited depth BFS exploration, up to XXX (an integer) steps from initial state.
+
+
+Consider that we intend to run the file *kangan10.gal*. For doing this, there are two different ways:
+
+**The first one:**
+
+Select the file *kangan10.gal* -> *Run As* -> *Run Configurations...* as follows:
+
+
+
+
+Then:
+create a new ITS Tools configuration
+
+
+
+
+In the Model selection tab:
+* edit the configuration name
+* select the project and the model file
+
+
+
+
+In the General Options tab, configure the tool according to your will
+
+
+
+
+
+And click on Run.
+
+
+**The second one:**
+
+You can also directly run the GAL model file as an ITS model-check as follows:
+
+
+
+
+
+To see the file configuration automatically generated (with the default values of the different options), you can repeat the first step of the previous method or use Run icon combo box in the toolbar as follows and then configure the tool accordingly:
+
+
diff --git a/itstools/docR.md b/itstools/docR.md
new file mode 100644
index 0000000000..1d8597c473
--- /dev/null
+++ b/itstools/docR.md
@@ -0,0 +1,129 @@
+---
+title: Configuration and Running of ITS_Tools from Eclipse
+---
+
+How to run ITS_Tools from Eclipse?
+=================================================
+
+This documentation aims to show you an interactive way to run ITS_Tools from Eclipse.
+
+Consider that we intend to run the file *kangan10.gal*. This you may do by:
+
+ * Running it directly with the *default options values* as they have been specified or by
+ * Configuring it first accordingly to your purposes before the running.
+
+
+1. The *right click* method:
+
+ You can perform it as described below:
+
+ 
+
+
+2. Running after Configuring
+
+ * Open the Eclipse Configuration window
+
+ **First way :** (right) click on the file *kangan10.gal* -> *Run As* -> *Run Configurations...*
+
+ 
+
+
+ **Second way :** Open the Run combo-box icon in the toolbar -> click Run Configurations...
+
+ 
+
+
+ * In the General Options tab, configure the tool according to your will
+
+ 
+
+
+ * click *Run*.
+
+
+
+ It is also possible to create manually a new configuration by following the steps below:
+
+ Right click on *ITS Tools* menu -> click *New*
+
+ 
+
+
+
+
+Then *Edit the configuration name and select a project and a model file (see Model Selection tab)*
+
+ 
+
+
+
+
+3. Reference Manual for Options (retained in the General Options tab)
+
+Several options have been chosen among all those available in the command-line its-tools version.
+They are:
++ Input options (mandatory):
+----------------------------
+
+ -i path : specifies the path to the input model file.
+
+ -t {CAMI|PROD|ROMEO|ITSXML|ETF|DVE|GAL|DLL|NDLL} : specifies format of the input model file :
+
+ CAMI : CAMI format (for P/T nets) is the native Petri net format of CPN-AMI
+ PROD : PROD format (for P/T nets) is the native format of PROD
+ ROMEO : an XML format (for Time Petri nets) that is the native format of Romeo
+ ITSXML : a native XML format (for ANY kind of ITS) for this tool. These files allow to point to other files and are used as main file for composite definitions. See this example, the list of formalism/format supported is described here.
+ ETF : Extended Table Format is the native format used by LTSmin, built from many front-ends.
+ DVE : Divine is a modelling language similar to Promela. Input file should be in Divine format.
+ GAL : Guarded Action Language. Input file should be in GAL syntax.
+ DLL : use a dynamic library that provides a function "void loadModel (Model &,int)" typically written using the manipulation APIs. See demo/ folder.
+ NDLL : same as DLL, but expect input formatted as size:lib.so. See demo/ folder for a usage example. Both DLL and NDLL are used to inject of arbitrary C++ ITS types into the ITSModel.
+
+
++ An option related to Variable Order:
+------------------------------------
+
+ --dump-order path : dump the currently used variable order to file designated by path and exit.
+
+ + Options related to Encoding of ITS types
+ -------------------------------------------
+
+ For Petri nets, there is a choice between an SDD encoding, where to each variable is associated the set of integer values it can take, or a DDD encoding, where each edge of the decision diagram is labeled by a single value (i.e. like MDD). The default used is the SDD encoding, but option --ddd sometimes works better when markings (or transition latest firing times) have large values.
+
+ --sdd : privilege SDD storage (Petri net models only).[DEFAULT]
+ --ddd : privilege DDD (no hierarchy) encoding (Petri net models only).
+
+ For Scalar and Circular symmetric composite types, the following options allow to use recursive state encodings. The default setting is "-ssD2 1", i.e. for a Scalar or Circular set of size n, define n SDD variables, one per subcomponent.
+
+ -ssD2 INT :[DEFAULT: -ssD2 1] (depth 2 levels) use 2 level depth for scalar sets. Integer provided defines level 2 block size.
+ -ssDR INT : (depth recursive) use recursive encoding for scalar sets. Integer provided defines number of blocks at highest levels.
+ -ssDS INT : (depth shallow recursive) use alternative recursive encoding for scalar sets. Integer provided defines number of blocks at lowest level.
+
+
++ Options related to gc policy
+-------------------------------
+
+ Garbage collection options :
+ --no-garbage : disable garbage collection (may be faster, more memory)
+ --gc-threshold INT : set the threshold for first starting to do gc [DEFAULT:13000 kB=1.3GB]
+
+ + Options related to saturation
+ --------------------------------
+
+ Two variants of saturation are possible, controlling how clusters are applied at a given level. The BFS variant chains application of each transition cluster using a round robin, while the DFS variant chains applications to a fixpoint of each cluster. The DFS variant can be very efficient when a given transition cluster can be fired several times in a row. This could be the case for a transition with a high level of non-determinism, or a transition such as "time elapses" which can often be chained without firing other transitions. Petri nets with large marking values also often exhibit this behavior where a transition can be fired several times in a row.
+
+ The default setting is BFS, except if loading Time Petri nets where the default becomes DFS (more efficient in our experiments). Manually setting the strategy overrules these defaults.
+
+ --fixpoint {BFS,DFS} : this options controls which kind of saturation algorithm is applied. Both are variants of saturation not really full DFS or BFS. [default: BFS]
+
+
++ An Option controlling the reachable set computation ( specific to its-reach)
+
+ The default behavior of its-reach is to build the full state space (which is hopefully finite), using saturation. This behavior can be changed to force a bounded BFS exploration (i.e. bounded model-checking or bmc) of the state space over a given number of steps.
+
+ -bmc XXX : use limited depth BFS exploration, up to XXX (an integer) steps from initial state.
+
+
+
+
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/.settings/org.eclipse.jdt.core.prefs b/itstools/fr.lip6.move.gal.itstools.launch/.settings/org.eclipse.jdt.core.prefs
index c537b63063..0c68a61dca 100644
--- a/itstools/fr.lip6.move.gal.itstools.launch/.settings/org.eclipse.jdt.core.prefs
+++ b/itstools/fr.lip6.move.gal.itstools.launch/.settings/org.eclipse.jdt.core.prefs
@@ -1,7 +1,7 @@
eclipse.preferences.version=1
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.6
-org.eclipse.jdt.core.compiler.compliance=1.6
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.8
+org.eclipse.jdt.core.compiler.compliance=1.8
org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
-org.eclipse.jdt.core.compiler.source=1.6
+org.eclipse.jdt.core.compiler.source=1.8
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/META-INF/MANIFEST.MF b/itstools/fr.lip6.move.gal.itstools.launch/META-INF/MANIFEST.MF
index 1c57eef69d..414a8a9aa0 100644
--- a/itstools/fr.lip6.move.gal.itstools.launch/META-INF/MANIFEST.MF
+++ b/itstools/fr.lip6.move.gal.itstools.launch/META-INF/MANIFEST.MF
@@ -1,6 +1,6 @@
Manifest-Version: 1.0
Bundle-ManifestVersion: 2
-Bundle-Name: Launch configurations for ITS tools
+Bundle-Name: Launch configuration for ITS tools
Bundle-SymbolicName: fr.lip6.move.gal.itstools.launch;singleton:=true
Bundle-Version: 1.0.0.qualifier
Bundle-Activator: fr.lip6.move.gal.itstools.launch.Activator
@@ -14,3 +14,4 @@ Require-Bundle: org.eclipse.debug.ui,
Bundle-RequiredExecutionEnvironment: JavaSE-1.8
Bundle-ActivationPolicy: lazy
Export-Package: fr.lip6.move.gal.itstools.launch
+Import-Package: org.eclipse.draw2d
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/CommandLineBuilder.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/CommandLineBuilder.java
index 6fe0325931..f16343c4e5 100644
--- a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/CommandLineBuilder.java
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/CommandLineBuilder.java
@@ -23,6 +23,7 @@
import fr.lip6.move.gal.Specification;
import fr.lip6.move.gal.instantiate.GALRewriter;
import fr.lip6.move.gal.itstools.CommandLine;
+import fr.lip6.move.gal.itstools.launch.devtools.ReachableFormula;
import fr.lip6.move.gal.itstools.preference.GalPreferencesActivator;
import fr.lip6.move.gal.itstools.preference.PreferenceConstants;
import fr.lip6.move.serialization.BasicGalSerializer;
@@ -40,14 +41,12 @@ public static CommandLine buildCommand(ILaunchConfiguration configuration) throw
-
// Produce a GAL file to give to its-tools
IPath oriPath = Path.fromPortableString(oriString);
// work folder
File workingDirectory ;
-
String cegarProp = configuration.getAttribute(LaunchConstants.CEGAR_PROP, "");
if (! "".equals(cegarProp)) {
// Path to ITS-reach exe
@@ -238,11 +237,12 @@ public static CommandLine buildCommand(ILaunchConfiguration configuration) throw
cl.addArg("--quiet");
}
+
}
-
-
- cl.setWorkingDir(workingDirectory);
+ cl.setWorkingDir(workingDirectory);
+ ReachableFormula.getInstance().addFlags(cl, configuration);
+ //System.out.println("\n"+cl);
return cl;
}
}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/ITSLaunchShortcut.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/ITSLaunchShortcut.java
index 04f6445fa3..12e7720763 100644
--- a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/ITSLaunchShortcut.java
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/ITSLaunchShortcut.java
@@ -24,6 +24,9 @@
import org.eclipse.ui.IWorkbench;
import org.eclipse.ui.IWorkbenchWindow;
import org.eclipse.ui.dialogs.ElementListSelectionDialog;
+
+import fr.lip6.move.gal.itstools.launch.devtools.ReachableFormula;
+
import org.eclipse.jface.dialogs.MessageDialog;
@@ -128,11 +131,18 @@ private ILaunchConfiguration createConfiguration (String modelff, IProject curPr
ILaunchConfiguration config = null;
try {
ILaunchConfigurationType configType = getConfigurationType();
- String modelname = new File(modelff).getName();
+ String modelname = new File
+ (modelff).getName();
ILaunchConfigurationWorkingCopy wc = configType.newInstance(null, DebugPlugin.getDefault().getLaunchManager().generateLaunchConfigurationName(modelname));
+// System.out.println("wc in launchShortCut" + wc);
+ // set default values for anew LaunchConfiguration
wc.setAttribute(LaunchConstants.PROJECT, curProj.getName());
wc.setAttribute(LaunchConstants.MODEL_FILE,modelff);
+
+ ReachableFormula.getInstance().setDefaults(wc);
+ //ReachFormula.setDefaultValue(wc);
+// wc.setAttribute(LaunchConstants.QUIET, true);
config = wc.doSave();
} catch (CoreException ce) {
MessageDialog.openError(getShell(), "Error creating launch configuration from shortcut.", ce.getStatus().getMessage());
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/ITSLaunchTabGroup.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/ITSLaunchTabGroup.java
index 1bcb3ef806..4478255416 100644
--- a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/ITSLaunchTabGroup.java
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/ITSLaunchTabGroup.java
@@ -1,13 +1,11 @@
package fr.lip6.move.gal.itstools.launch;
-import org.eclipse.core.resources.IProject;
-import org.eclipse.core.runtime.CoreException;
-import org.eclipse.debug.core.ILaunchConfiguration;
import org.eclipse.debug.ui.AbstractLaunchConfigurationTabGroup;
import org.eclipse.debug.ui.CommonTab;
import org.eclipse.debug.ui.ILaunchConfigurationDialog;
import org.eclipse.debug.ui.ILaunchConfigurationTab;
-import org.eclipse.debug.ui.WorkingDirectoryBlock;
+
+import fr.lip6.move.gal.itstools.launch.devtools.ReachableFormula;
public class ITSLaunchTabGroup extends AbstractLaunchConfigurationTabGroup {
@@ -18,7 +16,10 @@ public ITSLaunchTabGroup() {
@Override
public void createTabs(ILaunchConfigurationDialog dialog, String mode) {
- ILaunchConfigurationTab[] tabs = {new MainTab(), new CommonTab() };
+ ReachableFormula r = ReachableFormula.getInstance();
+ OptionsTab otab = new OptionsTab(r);
+
+ ILaunchConfigurationTab[] tabs = {new MainTab(), otab , new CommonTab() };
setTabs(tabs);
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/LaunchConstants.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/LaunchConstants.java
index af2850c40c..971dfd11dd 100644
--- a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/LaunchConstants.java
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/LaunchConstants.java
@@ -8,4 +8,5 @@ public class LaunchConstants {
public static final String PROJECT = "project";
public static final String PLAY_TRACE = "trace";
public static final String CEGAR_PROP = "cegar prop";
+ public static final String QUIET = "quiet";
}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/MainTab.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/MainTab.java
index 9cbdf304b3..e4581596a5 100644
--- a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/MainTab.java
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/MainTab.java
@@ -1,7 +1,5 @@
package fr.lip6.move.gal.itstools.launch;
-import java.io.File;
-
import org.eclipse.core.resources.IProject;
import org.eclipse.core.resources.ResourcesPlugin;
import org.eclipse.core.runtime.CoreException;
@@ -9,11 +7,8 @@
import org.eclipse.debug.core.ILaunchConfigurationWorkingCopy;
import org.eclipse.debug.internal.ui.SWTFactory;
import org.eclipse.debug.ui.AbstractLaunchConfigurationTab;
-import org.eclipse.jface.preference.DirectoryFieldEditor;
import org.eclipse.jface.preference.FieldEditorPreferencePage;
import org.eclipse.jface.preference.FileFieldEditor;
-import org.eclipse.jface.util.PropertyChangeEvent;
-import org.eclipse.jface.viewers.BaseLabelProvider;
import org.eclipse.jface.viewers.ILabelProvider;
import org.eclipse.jface.viewers.LabelProvider;
import org.eclipse.jface.window.Window;
@@ -32,6 +27,7 @@
import org.eclipse.swt.widgets.Text;
import org.eclipse.ui.dialogs.ElementListSelectionDialog;
+@SuppressWarnings("restriction")
public class MainTab extends AbstractLaunchConfigurationTab implements ModifyListener {
private static final String DEFAULT_MODEL_FILE = "model.gal";
@@ -154,6 +150,8 @@ protected void createProjectEditor(Composite parent) {
@Override
public void setDefaults(ILaunchConfigurationWorkingCopy configuration) {
+ //System.out.println("oraaaaammm\n\nbraaaaaoooommmmm");
+
configuration.setAttribute(LaunchConstants.MODEL_FILE, DEFAULT_MODEL_FILE);
}
@@ -166,6 +164,7 @@ public void initializeFrom(ILaunchConfiguration configuration) {
e.printStackTrace();
}
+
}
private IProject chooseProject() {
@@ -205,6 +204,12 @@ private IProject getProject() {
public void performApply(ILaunchConfigurationWorkingCopy configuration) {
configuration.setAttribute(LaunchConstants.PROJECT, fProjText.getText().trim());
configuration.setAttribute(LaunchConstants.MODEL_FILE, modelFileEditor.getStringValue());
+// try {
+// System.out.println(configuration.getWorkingCopy().getAttributes());
+// } catch (CoreException e) {
+// // TODO Auto-generated catch block
+// e.printStackTrace();
+// }
setDirty(false);
}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/OptionsTab.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/OptionsTab.java
new file mode 100644
index 0000000000..bc0e758c58
--- /dev/null
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/OptionsTab.java
@@ -0,0 +1,119 @@
+package fr.lip6.move.gal.itstools.launch;
+
+import org.eclipse.debug.core.ILaunchConfiguration;
+import org.eclipse.debug.core.ILaunchConfigurationWorkingCopy;
+import org.eclipse.debug.internal.ui.SWTFactory;
+import org.eclipse.debug.ui.AbstractLaunchConfigurationTab;
+import org.eclipse.swt.events.ModifyEvent;
+import org.eclipse.swt.events.SelectionEvent;
+import org.eclipse.swt.layout.GridData;
+import org.eclipse.swt.widgets.Composite;
+
+import fr.lip6.move.gal.itstools.launch.devtools.IFormula;
+import fr.lip6.move.gal.itstools.launch.devtools.IOption;
+import fr.lip6.move.gal.itstools.launch.devtools.IWidgetListener;
+import fr.lip6.move.gal.itstools.launch.devtools.ReachableFormula;
+
+@SuppressWarnings("restriction")
+public class OptionsTab extends AbstractLaunchConfigurationTab /*implements ModifyListener*/ {
+
+ private class WidgetListener implements IWidgetListener {
+
+ public void modifyText(ModifyEvent e) {
+ updateLaunchConfigurationDialog();
+ }
+
+ public void widgetDefaultSelected(SelectionEvent e) {
+ /* do nothing */}
+
+ public void widgetSelected(SelectionEvent e) {
+ updateLaunchConfigurationDialog();
+ }
+ }
+ private IFormula formula ;
+ public OptionsTab(IFormula formula) {
+ super();
+ this.formula = formula;
+ }
+
+
+
+ private IWidgetListener listener = new WidgetListener();
+
+ // LISTENER GENERAL
+
+
+
+ public void addOption(IOption option) {
+ formula.getOptions().add(option);
+ }
+
+ @Override
+ public void createControl(Composite parent) {
+ Composite main = SWTFactory.createComposite(parent, 1, 3, GridData.FILL_BOTH);
+
+ for (IOption opt : formula.getOptions()) {
+ opt.addControl(main, listener);
+ }
+
+ setControl(main);
+ }
+
+ @Override
+ public void setDefaults(ILaunchConfigurationWorkingCopy configuration) {
+ ReachableFormula.getInstance().setDefaults(configuration);
+ }
+
+ @Override
+ public void initializeFrom(ILaunchConfiguration configuration) {
+
+ for (IOption opt : formula.getOptions()) {
+ opt.initializeFrom(configuration);
+ }
+
+ }
+
+ @Override
+ public void performApply(ILaunchConfigurationWorkingCopy configuration) {
+
+ for (IOption opt : formula.getOptions()) {
+ opt.performApply(configuration);
+ }
+
+ // A RETIRER JUSTE POUR LE DEBUG
+// try {
+// System.out.println(configuration.getAttributes());
+// } catch (CoreException e) {
+// // TODO Auto-generated catch block
+// e.printStackTrace();
+// }
+
+ }
+
+ @Override
+ public void activated(ILaunchConfigurationWorkingCopy workingCopy) {return;
+ }
+
+ @Override
+ public void deactivated(ILaunchConfigurationWorkingCopy workingCopy) {return;
+ }
+
+ @Override
+ public String getName() {
+ return "General Options";
+ }
+
+ @Override
+ public boolean isValid(ILaunchConfiguration launchConfig) {
+ setErrorMessage(null);
+ for (IOption opt : formula.getOptions()) {
+ if (!opt.isValid(launchConfig)) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+
+
+}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/DefaultValueComputed.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/DefaultValueComputed.java
new file mode 100644
index 0000000000..54ba3dc4df
--- /dev/null
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/DefaultValueComputed.java
@@ -0,0 +1,36 @@
+package fr.lip6.move.gal.itstools.launch.devtools;
+
+import org.eclipse.core.runtime.CoreException;
+import org.eclipse.core.runtime.IPath;
+import org.eclipse.core.runtime.Path;
+import org.eclipse.debug.core.ILaunchConfiguration;
+
+import fr.lip6.move.gal.itstools.launch.LaunchConstants;
+
+public class DefaultValueComputed { //Peut évoluer en implantant une interface qui calcule des valeurs par défaut
+
+ private String extension;
+
+ public DefaultValueComputed(String extension) {
+ this.extension = extension;
+ }
+
+ public String computeConfigurationDefaultValue(ILaunchConfiguration configuration){
+ String oriString = null;
+ String defaultValue = null;
+ try {
+ oriString = configuration.getAttribute(LaunchConstants.MODEL_FILE, "model.gal");
+ } catch (CoreException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ }
+ IPath oriPath;
+ if (oriString != null){
+ oriPath= Path.fromPortableString(oriString);
+ defaultValue = oriPath.removeFileExtension().lastSegment() + extension;
+ }
+ return defaultValue;
+
+ }
+
+}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/IFormula.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/IFormula.java
new file mode 100644
index 0000000000..883628f7e1
--- /dev/null
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/IFormula.java
@@ -0,0 +1,15 @@
+package fr.lip6.move.gal.itstools.launch.devtools;
+
+import java.util.Collection;
+
+import org.eclipse.debug.core.ILaunchConfiguration;
+import org.eclipse.debug.core.ILaunchConfigurationWorkingCopy;
+
+import fr.lip6.move.gal.itstools.CommandLine;
+
+public interface IFormula {
+
+ public void setDefaults(ILaunchConfigurationWorkingCopy wc);
+ public void addFlags(CommandLine cl, ILaunchConfiguration configuration);
+ public Collection> getOptions();
+}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/IOption.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/IOption.java
new file mode 100644
index 0000000000..3b792eeb54
--- /dev/null
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/IOption.java
@@ -0,0 +1,25 @@
+package fr.lip6.move.gal.itstools.launch.devtools;
+
+
+
+import org.eclipse.debug.core.ILaunchConfiguration;
+import org.eclipse.debug.core.ILaunchConfigurationWorkingCopy;
+import org.eclipse.swt.widgets.Composite;
+
+import fr.lip6.move.gal.itstools.CommandLine;
+
+public interface IOption {
+
+ public String getName();
+ public String getToolTip();
+ public T getDefaultValue();
+
+
+ public void initializeFrom(ILaunchConfiguration configuration);
+ public void performApply(ILaunchConfigurationWorkingCopy configuration);
+
+ public void addControl(Composite composite, IWidgetListener listener);
+ public void addFlagsToCommandLine(CommandLine cl, ILaunchConfiguration configuration);
+ public void setDefaults(ILaunchConfigurationWorkingCopy wc);
+ public boolean isValid(ILaunchConfiguration launchConfig);
+}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/IWidgetListener.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/IWidgetListener.java
new file mode 100644
index 0000000000..610107a13f
--- /dev/null
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/IWidgetListener.java
@@ -0,0 +1,8 @@
+package fr.lip6.move.gal.itstools.launch.devtools;
+
+import org.eclipse.swt.events.ModifyListener;
+import org.eclipse.swt.events.SelectionListener;
+
+public interface IWidgetListener extends ModifyListener, SelectionListener {
+
+}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionBoolean.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionBoolean.java
new file mode 100644
index 0000000000..614952634c
--- /dev/null
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionBoolean.java
@@ -0,0 +1,117 @@
+package fr.lip6.move.gal.itstools.launch.devtools;
+
+import org.eclipse.core.runtime.CoreException;
+import org.eclipse.debug.core.ILaunchConfiguration;
+import org.eclipse.debug.core.ILaunchConfigurationWorkingCopy;
+import org.eclipse.debug.internal.ui.SWTFactory;
+import org.eclipse.swt.SWT;
+import org.eclipse.swt.layout.GridData;
+import org.eclipse.swt.layout.GridLayout;
+import org.eclipse.swt.widgets.Button;
+import org.eclipse.swt.widgets.Composite;
+
+import fr.lip6.move.gal.itstools.CommandLine;
+
+@SuppressWarnings("restriction")
+public class OptionBoolean implements IOption {
+
+ private boolean defaultValue;
+ private String name;
+ private String tooltiptext;
+ private Button button;
+ private String flag;
+
+ public OptionBoolean(String name, String tooltip, boolean defaultValue) {
+ this.defaultValue = defaultValue;
+ this.name = name;
+ tooltiptext = tooltip;
+ }
+
+ public OptionBoolean(String name, String tooltiptext) {
+ this.name = name;
+ this.tooltiptext = tooltiptext;
+ this.defaultValue = true;
+ }
+
+ @Override
+ public String getName() {
+ return name;
+ }
+
+ @Override
+ public Boolean getDefaultValue() {
+ return defaultValue;
+ }
+
+
+
+ @Override
+ public String getToolTip() {
+ return tooltiptext;
+ }
+
+ @Override
+ public void addControl(Composite composite, IWidgetListener listener) {
+ Composite check_composite = new Composite(composite, SWT.FILL);
+ GridLayout layout = new GridLayout(1, true);
+ check_composite.setLayout(layout);
+ button = SWTFactory.createCheckButton(check_composite, name, null, defaultValue, 2);
+ GridData layoutData = new GridData();
+ button.setLayoutData(layoutData);
+ button.setToolTipText(tooltiptext);
+ button.addSelectionListener(listener);
+ }
+
+ public Button getButton() {
+ return button;
+ }
+
+ @Override
+ public void initializeFrom(ILaunchConfiguration configuration) {
+ //System.out.println("Configuration " + configuration); TBR
+
+ Boolean currentValue;
+ try {
+ currentValue = configuration.getAttribute(name, false);
+ getButton().setSelection((Boolean) currentValue);
+ } catch (CoreException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ }
+
+ }
+
+ @Override
+ public void performApply(ILaunchConfigurationWorkingCopy configuration) {
+ boolean button_state = getButton().getSelection();
+ configuration.setAttribute(getName(), button_state);
+ }
+
+ public void setFlag(String flag) {
+ this.flag = flag;
+ }
+
+ @Override
+ public void addFlagsToCommandLine(CommandLine cl, ILaunchConfiguration configuration) {
+ try {
+ Boolean value = configuration.getAttribute(name, false);
+ if (value.booleanValue()) {
+ cl.addArg(flag);
+ }
+ } catch (CoreException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ }
+ }
+
+ @Override
+ public void setDefaults(ILaunchConfigurationWorkingCopy wc) {
+ wc.setAttribute(name, defaultValue);
+ }
+
+ @Override
+ public boolean isValid(ILaunchConfiguration launchConfig) {
+ return true;
+ }
+
+}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionEnum.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionEnum.java
new file mode 100644
index 0000000000..e3a6192d9d
--- /dev/null
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionEnum.java
@@ -0,0 +1,168 @@
+package fr.lip6.move.gal.itstools.launch.devtools;
+
+import java.util.HashMap;
+
+import org.eclipse.core.runtime.CoreException;
+import org.eclipse.debug.core.ILaunchConfiguration;
+import org.eclipse.debug.core.ILaunchConfigurationWorkingCopy;
+import org.eclipse.swt.SWT;
+import org.eclipse.swt.layout.GridData;
+import org.eclipse.swt.layout.GridLayout;
+import org.eclipse.swt.widgets.Combo;
+import org.eclipse.swt.widgets.Composite;
+import org.eclipse.swt.widgets.Label;
+
+import fr.lip6.move.gal.itstools.CommandLine;
+
+public class OptionEnum implements IOption {
+ private String flag;
+ private String defaultValue;
+ private String name;
+ private String tooltiptext;
+
+ private Combo combo;
+ private HashMap potentialValuesAndFlags;
+ public HashMap getPotentialValuesAndFlags() {
+ return potentialValuesAndFlags;
+ }
+
+
+ public void setFlag(String flag){
+ this.flag = flag;
+ }
+ public String getTooltiptext() {
+ return tooltiptext;
+ }
+
+ public void setTooltiptext(String tooltiptext) {
+ this.tooltiptext = tooltiptext;
+ }
+
+ public String[] getPotentialValues() {
+ return potentialValuesAndFlags.keySet().toArray(new String [potentialValuesAndFlags.size()]);
+ }
+
+ public void setCombo(Combo combo) {
+ this.combo = combo;
+ }
+
+
+ public OptionEnum(String name, String tooltiptext, String defaultValue ) {
+ this.defaultValue = defaultValue;
+ this.name = name;
+ this.tooltiptext = tooltiptext;
+ }
+
+ public void setPotentialValuesAndFlags(HashMap potentialValuesAndFlags) {
+ this.potentialValuesAndFlags = potentialValuesAndFlags;
+ }
+
+ @Override
+ public String getName() {
+ return name;
+ }
+
+ @Override
+ public String getToolTip() {
+ return tooltiptext;
+ }
+
+ @Override
+ public String getDefaultValue() {
+ return defaultValue;
+ }
+
+
+
+
+
+ public Combo getCombo() {
+ // TODO Auto-generated method stub
+ return combo;
+ }
+
+ @Override
+ public void initializeFrom(ILaunchConfiguration configuration) {
+ Object currentValue;
+ try {
+ currentValue = configuration.getAttributes().get(name);
+ if(currentValue != null)
+ getCombo().setText((String)currentValue);
+ } catch (CoreException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ }
+ }
+
+ @Override
+ public void performApply(ILaunchConfigurationWorkingCopy configuration) {
+ String combo_state = getCombo().getText();
+ configuration.setAttribute(getName(), combo_state);
+
+ }
+
+ @Override
+ public void addControl(Composite composite, IWidgetListener listener) {
+ Composite label_combo_composite = new Composite(composite, 0);
+
+// RowLayout rowLayout = new RowLayout();
+// RowData rowdata = new RowData();
+// rowdata.
+ GridLayout layout = new GridLayout();
+ layout.numColumns = 2;
+ label_combo_composite.setLayout(layout);
+// GridData gridData = new GridData(GridData.FILL_HORIZONTAL);
+// gridData.horizontalSpan = 2;
+ //label_combo_composite.setLayoutData(gridData);
+ //label_combo_composite.setLayout(layout);
+// rowLayout.pack = false;
+// rowLayout.justify = true;
+ //label_combo_composite.setLayout(rowLayout);
+ Label label = new Label(label_combo_composite, SWT.NONE);
+
+ GridData g = new GridData(SWT.RIGHT);
+ label.setLayoutData(g);
+ GridData g1 = new GridData(SWT.RIGHT);
+ //g.horizontalAlignment = GridData.FILL;
+ //label.setLayoutData(g);
+ label.setText(name);
+ label.setToolTipText(tooltiptext);
+ combo = new Combo(label_combo_composite, SWT.RIGHT);
+
+ // combo.setLayoutData(g);
+ combo.setLayoutData(g1);
+ combo.setItems(getPotentialValues());
+ combo.addSelectionListener(listener);
+ }
+
+ @Override
+ public void addFlagsToCommandLine(CommandLine cl, ILaunchConfiguration configuration) {
+ try {
+ String value = configuration.getAttribute(name, "");
+ if (value.length() > 0){
+ if (flag != null) // utile dans OptionEnumWithText dont la method addFlag to Command appelle la méthode ici
+ cl.addArg(flag);
+ //System.out.println("hhhhhhhhh\n\n" +value);
+ String flagValue = potentialValuesAndFlags.get(value);
+ if (flagValue != null)
+ cl.addArg(flagValue);
+ }
+ } catch (CoreException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ }
+
+ }
+ @Override
+ public void setDefaults(ILaunchConfigurationWorkingCopy wc){
+ wc.setAttribute(name, defaultValue);
+ }
+ @Override
+ public boolean isValid(ILaunchConfiguration launchConfig) { // Detecte uniquement la saisie d'un valeur par défaut n'appartenant pas à la liste des potentialvalues
+ for (String s : getPotentialValues())
+ if (s.equals(combo.getText()))
+ return true;
+ return false;
+ }
+
+}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionEnumWithText.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionEnumWithText.java
new file mode 100644
index 0000000000..6e9edaa080
--- /dev/null
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionEnumWithText.java
@@ -0,0 +1,136 @@
+package fr.lip6.move.gal.itstools.launch.devtools;
+
+import org.eclipse.core.runtime.CoreException;
+import org.eclipse.debug.core.ILaunchConfiguration;
+import org.eclipse.debug.core.ILaunchConfigurationWorkingCopy;
+import org.eclipse.swt.SWT;
+import org.eclipse.swt.layout.GridData;
+import org.eclipse.swt.layout.GridLayout;
+import org.eclipse.swt.widgets.Combo;
+import org.eclipse.swt.widgets.Composite;
+import org.eclipse.swt.widgets.Label;
+import org.eclipse.swt.widgets.Text;
+
+import fr.lip6.move.gal.itstools.CommandLine;
+
+public class OptionEnumWithText extends OptionEnum {
+
+ private Text addedText;
+ private String textValue;
+ private String text_state;
+
+ public OptionEnumWithText(String name, String tooltiptext, String defaultValue, String textValue) {
+ super(name, tooltiptext, defaultValue);
+ this.textValue = textValue;
+ text_state = textValue;
+ // TODO Auto-generated constructor stub
+ }
+
+ @Override
+ public void addControl(Composite composite, IWidgetListener listener) {
+ Composite label_combo_text_composite = new Composite(composite, 0);
+ GridLayout layout = new GridLayout(3, true);
+ label_combo_text_composite.setLayout(layout);
+ Label label = new Label(label_combo_text_composite, SWT.WRAP);
+ label.setText(getName());
+ label.setToolTipText(getTooltiptext());
+ setCombo(new Combo(label_combo_text_composite, SWT.NONE));
+ getCombo().setItems(getPotentialValues());
+ addedText = new Text(label_combo_text_composite, 0);
+ addedText.setLayoutData(new GridData());
+ getCombo().addSelectionListener(listener);
+ getAddedText().addModifyListener(listener);
+
+ }
+
+ @Override
+ public void initializeFrom(ILaunchConfiguration configuration) {
+ Object currentValue;
+ Object currentValueText;
+ try {
+ currentValue = configuration.getAttributes().get(getName());
+ currentValueText = configuration.getAttributes().get(getName() + "Value");
+ if (currentValue != null) {
+ getCombo().setText((String) currentValue);
+ } else {
+ getCombo().setText(getDefaultValue());
+ }
+ // En général ça aurait pu être une liste mais il aurait fallu fixer
+ // la place de la valeur-combo et celle du texte
+ if (currentValueText != null) {
+ addedText.setText((String) currentValueText);
+ } else {
+ getAddedText().setText(textValue);
+ }
+
+ } catch (CoreException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ }
+ }
+
+ @Override
+ public void performApply(ILaunchConfigurationWorkingCopy configuration) {
+ String combo_text_state = getCombo().getText();
+ text_state = getAddedText().getText();
+ configuration.setAttribute(getName(), combo_text_state);
+ configuration.setAttribute(getName() + "Value", text_state);
+ }
+
+ public Text getAddedText() {
+ return addedText;
+ }
+
+ @Override
+ public void addFlagsToCommandLine(CommandLine cl, ILaunchConfiguration configuration) {
+
+ String value;
+ try {
+ value = configuration.getAttribute(getName(), "");
+
+ if (value.length() > 0) {
+ String flagValue = getPotentialValuesAndFlags().get(value);
+ boolean flagAdded = false;
+ if (flagValue != null) {
+ cl.addArg(flagValue);
+ flagAdded = true;
+ }
+
+ // super.addFlagsToCommandLine(cl, configuration);
+ if (flagAdded && text_state != null)
+ cl.addArg(text_state);
+ }
+ } catch (CoreException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ }
+ }
+
+ public void setDefaults(ILaunchConfigurationWorkingCopy wc) {
+ super.setDefaults(wc);
+ wc.setAttribute(getName() + "Value", text_state);
+ }
+
+ @Override
+ public boolean isValid(ILaunchConfiguration launchConfig) {
+ boolean validEnumChoice = false;
+ for (String s : getPotentialValues())
+ if (s.equals(getCombo().getText())) {
+ validEnumChoice = true;
+ break;
+ }
+ if (validEnumChoice) {
+ try {
+ Double.parseDouble(getAddedText().getText());
+ } catch (NumberFormatException nfe) {
+ System.err.println(getAddedText().getText() + " is not a number!");
+ return false;
+ }
+ } else {
+ return false;
+ }
+
+ return true;
+ }
+
+}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionSeparator.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionSeparator.java
new file mode 100644
index 0000000000..c701690ce5
--- /dev/null
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionSeparator.java
@@ -0,0 +1,87 @@
+package fr.lip6.move.gal.itstools.launch.devtools;
+
+import org.eclipse.debug.core.ILaunchConfiguration;
+import org.eclipse.debug.core.ILaunchConfigurationWorkingCopy;
+import org.eclipse.swt.SWT;
+import org.eclipse.swt.graphics.Font;
+import org.eclipse.swt.graphics.FontData;
+import org.eclipse.swt.layout.GridData;
+import org.eclipse.swt.widgets.Composite;
+import org.eclipse.swt.widgets.Label;
+
+import fr.lip6.move.gal.itstools.CommandLine;
+
+public class OptionSeparator implements IOption {
+
+ private String name;
+
+ private String tooltiptext;
+ private Label separator;
+ public OptionSeparator(String name, String tooltip) {
+
+ this.name = name;
+ tooltiptext = tooltip;
+ }
+ @Override
+ public String getName() {
+
+ return name;
+ }
+
+ @Override
+ public String getToolTip() {
+ // TODO Auto-generated method stub
+ return tooltiptext;
+ }
+
+ @Override
+ public String getDefaultValue() {
+ // TODO Auto-generated method stub
+ return null;
+ }
+
+
+
+ @Override
+ public void initializeFrom(ILaunchConfiguration configuration) {
+ // TODO Auto-generated method stub
+
+ }
+
+ @Override
+ public void performApply(ILaunchConfigurationWorkingCopy configuration) {
+ // TODO Auto-generated method stub
+
+ }
+
+ @Override
+ public void addControl(Composite composite, IWidgetListener listener) {
+ Label description = new Label(composite,SWT.NULL);
+ description.setText(name);
+ Font boldFont = new Font(description.getDisplay(), new FontData("Arial", 11, SWT.BOLD|SWT.ITALIC));
+ description.setFont(boldFont);
+
+ separator= new Label(composite, SWT.SEPARATOR | SWT.HORIZONTAL);
+ GridData layoutData = new GridData(GridData.FILL_HORIZONTAL);
+ separator.setLayoutData(layoutData );
+ description.setToolTipText(tooltiptext);
+
+ }
+
+ @Override
+ public void addFlagsToCommandLine(CommandLine cl, ILaunchConfiguration configuration) {
+ // TODO Auto-generated method stub
+
+ }
+ @Override
+ public void setDefaults(ILaunchConfigurationWorkingCopy wc) {
+ // TODO Auto-generated method stub
+
+ }
+ @Override
+ public boolean isValid(ILaunchConfiguration launchConfig) {
+ // TODO Auto-generated method stub
+ return true;
+ }
+
+}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionText.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionText.java
new file mode 100644
index 0000000000..dfbe46f755
--- /dev/null
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/OptionText.java
@@ -0,0 +1,189 @@
+package fr.lip6.move.gal.itstools.launch.devtools;
+
+import org.eclipse.core.runtime.CoreException;
+import org.eclipse.debug.core.ILaunchConfiguration;
+import org.eclipse.debug.core.ILaunchConfigurationWorkingCopy;
+import org.eclipse.swt.SWT;
+import org.eclipse.swt.events.SelectionEvent;
+import org.eclipse.swt.events.SelectionListener;
+import org.eclipse.swt.layout.GridData;
+import org.eclipse.swt.layout.GridLayout;
+import org.eclipse.swt.widgets.Button;
+import org.eclipse.swt.widgets.Composite;
+import org.eclipse.swt.widgets.Text;
+
+import fr.lip6.move.gal.itstools.CommandLine;
+
+public class OptionText implements IOption {
+
+ private String defaultValue;
+ private String name;
+ private String tooltiptext;
+ private Text text;
+
+ private Button check;
+ private DefaultValueComputed computer;
+ private String flag;
+ private String text_state;
+
+ public void setFlag(String flag){
+ this.flag = flag;
+ }
+ public void setPathExtension(String extension) {
+ computer = new DefaultValueComputed(extension);
+ }
+
+ public void setText(Text text) {
+ this.text = text;
+ }
+
+ public OptionText( String name, String tooltiptext,String defaultValue) {
+ this.defaultValue = defaultValue;
+ text_state = defaultValue;
+ this.name = name;
+ this.setTooltiptext(tooltiptext);
+ }
+
+ @Override
+ public String getName() {
+ return name;
+ }
+
+ @Override
+ public String getToolTip() {
+ return getTooltiptext();
+ }
+
+ @Override
+ public String getDefaultValue() {
+ return defaultValue;
+ }
+
+ public Text getText() {
+ return text;
+ }
+
+ public String getTooltiptext() {
+ return tooltiptext;
+ }
+
+ public void setTooltiptext(String tooltiptext) {
+ this.tooltiptext = tooltiptext;
+ }
+
+ @Override
+ public void initializeFrom(ILaunchConfiguration configuration) {
+ Object currentValue;
+ try {
+
+ currentValue = configuration.getAttributes().get(name);
+ if(currentValue != null) {
+ getText().setText((String)currentValue);
+ check.setSelection(true);
+ }
+ else{
+
+ if (computer != null)
+ getText().setText(computer.computeConfigurationDefaultValue(configuration));
+
+ getText().setEnabled(false);
+
+ check.setSelection(false);
+ }
+ } catch (CoreException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ }
+
+ }
+
+ @Override
+ public void performApply(ILaunchConfigurationWorkingCopy configuration) {
+ if (!check.getSelection()){ // or getText().isEnabled()!
+ configuration.removeAttribute(getName());
+ getText().setEnabled(false);
+ return;
+ }
+ //String text_state = getText().getText();
+ text_state = getText().getText();
+
+ configuration.setAttribute(getName(), text_state);
+
+ }
+
+ @Override
+ public void addControl(Composite composite, IWidgetListener listener) {
+
+ Composite check_text_composite = new Composite(composite, SWT.FILL);
+ GridLayout layout = new GridLayout(2, true); //
+ //check_text_composite.setLayoutData(new GridData(1000, 50)); //
+ check_text_composite.setLayout(layout);
+ check = new Button(check_text_composite, SWT.CHECK);
+ //check.setSelection(true);
+ //setText(new ITS_Text(check_text_composite, 0)); //style 0 par défaut
+ check.setText(getName());
+ check.setToolTipText(getTooltiptext());
+ check.addSelectionListener(new SelectionListener() {
+
+ @Override
+ public void widgetSelected(SelectionEvent e) {
+
+ getText().setEnabled(check.getSelection());
+
+
+ }
+
+ @Override
+ public void widgetDefaultSelected(SelectionEvent arg0) {
+ return;
+ }
+ });
+
+ text = new Text(check_text_composite, 0);
+ text.setLayoutData(new GridData());
+// Text tmp = new Text(check_text_composite, 0);
+// GridData layoutData = new GridData(50, 50);
+// layoutData.horizontalAlignment = SWT.END;
+// tmp.setLayoutData(layoutData);;
+ check.addSelectionListener(listener);
+ text.addModifyListener(listener);
+ }
+
+ @Override
+ public void addFlagsToCommandLine(CommandLine cl, ILaunchConfiguration configuration) {
+ try {
+ String value = configuration.getAttribute(name, "");
+
+ if (value.length() > 0){
+ cl.addArg(flag);
+ //cl.addArg(text.getText());
+ cl.addArg(text_state);
+ }
+ } catch (CoreException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ }
+
+ }
+ @Override
+ public void setDefaults(ILaunchConfigurationWorkingCopy wc){
+ if (defaultValue != null)
+ wc.setAttribute(name, defaultValue);
+ //check.setSelection(true);
+ }
+ @Override
+ public boolean isValid(ILaunchConfiguration launchConfig) {
+ //Supposons que les champs doivent remplies par des entiers à l'exception des option possédant un computer
+ if (computer == null){
+ try {
+ if (check.getSelection())
+ Double.parseDouble(getText().getText());
+ } catch(NumberFormatException nfe) {
+ System.err.println(getText().getText() + " is not a number!");
+ return false;
+ }
+ }
+ return true;
+ }
+
+}
diff --git a/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/ReachableFormula.java b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/ReachableFormula.java
new file mode 100644
index 0000000000..a0591d7671
--- /dev/null
+++ b/itstools/fr.lip6.move.gal.itstools.launch/src/fr/lip6/move/gal/itstools/launch/devtools/ReachableFormula.java
@@ -0,0 +1,179 @@
+package fr.lip6.move.gal.itstools.launch.devtools;
+
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.LinkedList;
+import java.util.List;
+
+import org.eclipse.debug.core.ILaunchConfiguration;
+import org.eclipse.debug.core.ILaunchConfigurationWorkingCopy;
+
+import fr.lip6.move.gal.itstools.CommandLine;
+
+public class ReachableFormula implements IFormula {
+
+ private static List> options = new LinkedList<>();
+
+ private static ReachableFormula formula;
+
+ private ReachableFormula() {
+
+ }
+
+ public static ReachableFormula getInstance() {
+ if (formula == null) {
+ formula = new ReachableFormula();
+ instanciate();
+ }
+ return formula;
+
+ }
+
+ @Override
+ public Collection> getOptions() {
+ // TODO Auto-generated method stub
+ return options;
+ }
+
+ private static void instanciate() {
+
+ addVerbosityOptions();
+
+ addMemoryOptions();
+
+ addSpecialRunOptions();
+
+ addEncodingOptions();
+ }
+
+ private static void addSpecialRunOptions() {
+ OptionSeparator separator3 = new OptionSeparator("Special execution options",
+ "Flags that control what is computed");
+ options.add(separator3);
+
+ OptionText bmc = new OptionText("bmc",
+ "bmc XXX : use limited depth BFS exploration, only explore up to XXX steps from initial state", null);
+ bmc.setFlag("-bmc");
+
+ OptionText dump_order_path = new OptionText("dump-order path",
+ "dump the currently used variable order to file designated by path and exit", null);
+ dump_order_path.setPathExtension(".txt");
+ dump_order_path.setFlag("--dump-order");
+
+ options.add(dump_order_path);
+ options.add(bmc);
+ }
+
+ private static void addVerbosityOptions() {
+ OptionSeparator separator3 = new OptionSeparator("Verbosity Options",
+ "Flags that control the output of the tool");
+ options.add(separator3);
+
+ OptionText path = new OptionText("Export state space to a .dot file.",
+ "Exports the final state space SDD/DDD representation as GraphViz dot files. Specify the path prefix to construct dot state-space graph in.",
+ null);
+ path.setPathExtension(".dot");
+ path.setFlag("-d");
+
+ OptionBoolean quiet = new OptionBoolean("Quiet flag, to limit verbosity.",
+ "limit output verbosity useful in conjunction with te output --textline for batch performance runs",
+ true);
+ quiet.setFlag("--quiet");
+
+ OptionBoolean no_witness = new OptionBoolean("Do not compute witness traces",
+ "disable trace computation and just return a yes/no answer(faster).");
+ no_witness.setFlag("--nowitness");
+ OptionBoolean trace_states = new OptionBoolean(
+ "In any reported trace, also report intermediate states in the trace ?",
+ "if set, this option will force to print intermediate states (up to print limit) when showing traces. Default behavior is to only print a trace as a list of transition names.",
+ true);
+ trace_states.setFlag("--trace-states");
+ OptionText print_limit = new OptionText("Set the maximal size of state sets reported in the trace",
+ "State sets with less than this limit will be printed in extenso. DD holding more states will just print their size.",
+ "10");
+ print_limit.setFlag("--print-limit");
+
+ OptionBoolean stats = new OptionBoolean("Show statistics on final state space.",
+ "Produces stats on max sum of variables (i.e. maximum tokens in a marking for a Petri net), maximum variable value (bound for a Petri net)",
+ true);
+ stats.setFlag("--stats");
+ OptionBoolean edgeStat = new OptionBoolean("Show edge count statistics",
+ "Reports the size of the transition relation, i.e the number of unique source to target state pairs it contains.",
+ true);
+ edgeStat.setFlag("--edgeCount");
+
+ options.add(quiet);
+ options.add(path);
+ options.add(trace_states);
+ options.add(print_limit);
+ options.add(stats);
+ options.add(edgeStat);
+ options.add(no_witness);
+ }
+
+ private static void addEncodingOptions() {
+ OptionSeparator separator2 = new OptionSeparator("Encoding Options",
+ "Flags that control symbolic encoding of the system");
+ options.add(separator2);
+
+ OptionEnum sdd_ddd = new OptionEnum("Privilege SDD (hierarchy) or flat DDD ?",
+ "sdd : privilege SDD storage (Petri net models only\nddd : privilege DDD (no hierarchy) encoding (Petri net models only)",
+ "sdd");
+ HashMap sdd_ddd_map = new HashMap();
+ sdd_ddd_map.put("sdd", "--sdd");
+ sdd_ddd_map.put("ddd", "--ddd");
+ sdd_ddd.setPotentialValuesAndFlags(sdd_ddd_map);
+
+ OptionEnum fixpoint = new OptionEnum("Saturation fixpoint variant",
+ "This option controls how the saturation algorithm is applied : BFS iterates over transitions at each level, while DFS attempts to exploit self-chaining. Both are variants of saturation not really full DFS or BFS",
+ "BFS");
+ fixpoint.setFlag("--fixpoint");
+ HashMap fixpoint_map = new HashMap();
+ fixpoint_map.put("BFS", "BFS");
+ fixpoint_map.put("DFS", "DFS");
+ fixpoint.setPotentialValuesAndFlags(fixpoint_map);
+
+ OptionEnumWithText ssD = new OptionEnumWithText("Use recursive encodings for Scalar with block size :",
+ " -ssD2 INT : (depth 2 levels) use 2 level depth for scalar sets. Integer provided defines level 2 block size. [DEFAULT: -ssD2 1]\n-ssDR INT : (depth recursive) use recursive encoding for scalar sets. Integer provided defines number of blocks at highest levels.\n-ssDS INT : (depth shallow recursive) use alternative recursive encoding for scalar sets. Integer provided defines number of blocks at lowest level.",
+ "D2", "1");
+ HashMap ssD_map = new HashMap();
+ ssD_map.put("D2", "-ssD2");
+ ssD_map.put("DR", "-ssDR");
+ ssD_map.put("DS", "-ssDS");
+ ssD.setPotentialValuesAndFlags(ssD_map);
+
+ options.add(sdd_ddd);
+ options.add(fixpoint);
+ options.add(ssD);
+ }
+
+ private static void addMemoryOptions() {
+ OptionSeparator separator1 = new OptionSeparator("Memory Options",
+ "Flags that control memory usage and garbage collection ");
+ options.add(separator1);
+ OptionBoolean no_garbage = new OptionBoolean("Avoid any garbage collection",
+ "Disable garbage collection (may be faster, more memory), not usually a good idea.", false);
+ no_garbage.setFlag("--no-garbage");
+ OptionText gc_threshold = new OptionText("Start GC at resident memory (in GB):",
+ "Set the threshold for first trigger of gc (value in GigaBytes)", "1.3");
+ gc_threshold.setFlag("--gc-threshold");
+ options.add(no_garbage);
+ options.add(gc_threshold);
+ }
+
+ @Override
+ public void addFlags(CommandLine cl, ILaunchConfiguration configuration) {
+
+ for (IOption opt : options) {
+ opt.addFlagsToCommandLine(cl, configuration);
+ }
+ }
+
+ @Override
+ public void setDefaults(ILaunchConfigurationWorkingCopy wc){
+
+ for (IOption opt : options){
+ opt.setDefaults(wc);
+ }
+ }
+}
diff --git a/itstools/general_options.png b/itstools/general_options.png
new file mode 100644
index 0000000000..f5da7951d1
Binary files /dev/null and b/itstools/general_options.png differ
diff --git a/itstools/model_selection.png b/itstools/model_selection.png
new file mode 100644
index 0000000000..fe23ff4d3a
Binary files /dev/null and b/itstools/model_selection.png differ
diff --git a/itstools/new.png b/itstools/new.png
new file mode 100644
index 0000000000..873998d732
Binary files /dev/null and b/itstools/new.png differ
diff --git a/itstools/run_config.png b/itstools/run_config.png
new file mode 100644
index 0000000000..b201077c6c
Binary files /dev/null and b/itstools/run_config.png differ
diff --git a/itstools/run_icon.png b/itstools/run_icon.png
new file mode 100644
index 0000000000..87036094cb
Binary files /dev/null and b/itstools/run_icon.png differ
diff --git a/itstools/run_its_model_check.png b/itstools/run_its_model_check.png
new file mode 100644
index 0000000000..098db226f8
Binary files /dev/null and b/itstools/run_its_model_check.png differ