D-VerT version 0.2.0

Client: - remove ae2zot from supported plugins - fixed shortcut problem Server: - restore failureRatesBehaviour formulae
dice-project · Mar 18, 2017 · 33802ca · 33802ca
1 parent 7b5f043
commit 33802ca
Show file tree

Hide file tree

Showing 27 changed files with 47 additions and 57 deletions.
diff --git a/d-vert-server/d-vert-json2mc/json2mc/json2mc.py b/d-vert-server/d-vert-json2mc/json2mc/json2mc.py
@@ -14,7 +14,7 @@
 
 @author:     Francesco Marconi
 
-@copyright:  2016 Politecnico di Milano. All rights reserved.
+@copyright:  2015-2017 Politecnico di Milano. All rights reserved.
 
 @license:    Apache License 2.0
 
@@ -35,9 +35,9 @@
 from factory_methods import DiaVerificationFactory
 
 __all__ = []
-__version__ = "0.2"
-__date__ = '2016-12-19'
-__updated__ = '2017-01-25'
+__version__ = "0.2.0"
+__date__ = '2015-11-10'
+__updated__ = '2017-03-18'
 
 DEBUG = 0
 TESTRUN = 0
@@ -85,7 +85,7 @@ def main(argv=None):  # IGNORE:C0111
     program_license = '''%s
 
   Created by Francesco Marconi on %s.
-  Copyright 2016 Politecnico di Milano. All rights reserved.
+  Copyright 2015-2017 Politecnico di Milano. All rights reserved.
 
   Licensed under the Apache License 2.0
   http://www.apache.org/licenses/LICENSE-2.0
@@ -113,10 +113,12 @@ def main(argv=None):  # IGNORE:C0111
                             help="path to template file")
         group1.add_argument("-c", "--context", dest="context_path",
                             help="path to JSON context file"
-                            " [default: {}s]".format(os.path.join(base_dir,
+                            " [default: {}s]"
+                            .format(os.path.join(base_dir,
                                                  "context_examples",
                                                  "[{}]".format(", ".join(cfg.TECH_KEYS)),
-                                                 "[{}]_example.json".format(", ".join(cfg.TECH_KEYS)))))
+                                                 "[{}]_example.json"
+                                                 .format(", ".join(cfg.TECH_KEYS)))))
         parser.add_argument("-l", "--label", dest="label",
                             action="store_true",
                             help="apply graph labeling to reduce the size of "
@@ -179,7 +181,7 @@ def main(argv=None):  # IGNORE:C0111
                                                                    template_path=template_path,
                                                                    context=context,
                                                                    output_dir=output_dir,
-                                                                   display=display)                        
+                                                                   display=display)
                     print v_task
                     v_task.launch_verification()
                     if v_task.result_dir:

diff --git a/d-vert-server/d-vert-json2mc/json2mc/templates/storm_tl_template.lisp b/d-vert-server/d-vert-json2mc/json2mc/templates/storm_tl_template.lisp
@@ -1177,10 +1177,10 @@
 					(f-singleBoltsBehaviour the-bolts)
 					(f-singleQueueBehaviour the-bolts the-topology-table)
 					(f-ratesBehaviour the-spouts the-bolts the-topology-table)
-;					(f-failureRatesBehaviour the-spouts the-bolts the-impacts-table)
+					(f-failureRatesBehaviour the-spouts the-bolts the-impacts-table)
 					(f-clocks-behaviour the-spouts the-bolts the-proc-time-table)
 					(f-spoutClocksBehaviour the-spouts the-proc-time-table)
-					(f-noFailures '({{ topology.bolts|join(' ', attribute='id') }}))
+					(f-noFailures the-bolts)
 ;          (f-queueConstraint the-bolts QUEUE_THRESHOLD)
 				)
 			))
@@ -1202,10 +1202,10 @@
 		:logic :QF_UFRDL
 		:over-clocks MAX_TIME
 		:parametric-regions 't
-        {% if verification_params.strictly_monotonic_queues | length %}
-        :smt-assumptions "(and {% for s in verification_params.strictly_monotonic_queues %}(= (r_add_{{s.lower()}} i-loop) (r_add_{{s.lower()}} {{verification_params.num_steps + 1}})){%endfor%})"
-        {% endif %}
-        ;:smt-assumptions "(= (r_add_EXPANDER i-loop) (r_add_EXPANDER (+ {{verification_params.num_steps}} 1)))"
+		{% if verification_params.strictly_monotonic_queues | length %}
+		:smt-assumptions "(and {% for s in verification_params.strictly_monotonic_queues %}(= (r_add_{{s.lower()}} i-loop) (r_add_{{s.lower()}} {{verification_params.num_steps + 1}})){%endfor%})"
+		{% endif %}
+		;:smt-assumptions "(= (r_add_EXPANDER i-loop) (r_add_EXPANDER (+ {{verification_params.num_steps}} 1)))"
 		:discrete-counters (gen-counters-list the-spouts the-bolts the-impacts-table)
     {%  if verification_params.periodic_queues | length %}
     :l-monotonic '(Q_{{ verification_params.periodic_queues | join(' Q_') }})

diff --git a/plugin/it.polimi.dice.core.ui/META-INF/MANIFEST.MF b/plugin/it.polimi.dice.core.ui/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: DICE Core UI
 Bundle-SymbolicName: it.polimi.dice.core.ui;singleton:=true
-Bundle-Version: 0.1.1.qualifier
+Bundle-Version: 0.2.0.qualifier
 Bundle-Activator: it.polimi.dice.core.ui.DiceCoreUiPlugin
 Require-Bundle: org.eclipse.core.runtime,
  org.eclipse.core.resources,

diff --git a/plugin/it.polimi.dice.core.ui/pom.xml b/plugin/it.polimi.dice.core.ui/pom.xml
@@ -9,7 +9,7 @@
 	<parent>
 		<groupId>it.polimi.dice</groupId>
 		<artifactId>it.polimi.dice.parent</artifactId>
-	<version>0.1.1-SNAPSHOT</version>
+	<version>0.2.0-SNAPSHOT</version>
 	</parent>
 	<properties>
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

diff --git a/plugin/it.polimi.dice.core/META-INF/MANIFEST.MF b/plugin/it.polimi.dice.core/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: Dice Core Plugin
 Bundle-SymbolicName: it.polimi.dice.core;singleton:=true
-Bundle-Version: 0.1.1.qualifier
+Bundle-Version: 0.2.0.qualifier
 Bundle-Activator: it.polimi.dice.core.DiceCorePlugin
 Require-Bundle: org.eclipse.core.runtime
 Bundle-RequiredExecutionEnvironment: JavaSE-1.8

diff --git a/plugin/it.polimi.dice.core/pom.xml b/plugin/it.polimi.dice.core/pom.xml
@@ -9,7 +9,7 @@
 	<parent>
 		<groupId>it.polimi.dice</groupId>
 		<artifactId>it.polimi.dice.parent</artifactId>
-		<version>0.1.1-SNAPSHOT</version>
+		<version>0.2.0-SNAPSHOT</version>
 	</parent>
 	<properties>
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

diff --git a/plugin/it.polimi.dice.update/category.xml b/plugin/it.polimi.dice.update/category.xml
@@ -1,12 +1,12 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <site>
-   <feature url="features/it.polimi.dice.verification.feature_0.1.1.qualifier.jar" id="it.polimi.dice.verification.feature" version="0.1.1.qualifier">
+   <feature url="features/it.polimi.dice.verification.feature_0.2.0.qualifier.jar" id="it.polimi.dice.verification.feature" version="0.2.0.qualifier">
       <category name="it.polimi.dice.verification"/>
    </feature>
-   <feature url="features/it.polimi.dice.verification.ui.feature_0.1.1.qualifier.jar" id="it.polimi.dice.verification.ui.feature" version="0.1.1.qualifier">
+   <feature url="features/it.polimi.dice.verification.ui.feature_0.2.0.qualifier.jar" id="it.polimi.dice.verification.ui.feature" version="0.2.0.qualifier">
       <category name="it.polimi.dice.verification"/>
    </feature>
-   <feature url="features/it.polimi.dice.verification.uml2json.feature_0.1.1.qualifier.jar" id="it.polimi.dice.verification.uml2json.feature" version="0.1.1.qualifier">
+   <feature url="features/it.polimi.dice.verification.uml2json.feature_0.2.0.qualifier.jar" id="it.polimi.dice.verification.uml2json.feature" version="0.2.0.qualifier">
       <category name="it.polimi.dice.verification"/>
    </feature>
    <category-def name="it.polimi.dice.verification" label="DICE - Verification"/>

diff --git a/plugin/it.polimi.dice.update/pom.xml b/plugin/it.polimi.dice.update/pom.xml
@@ -9,6 +9,6 @@
 	<parent>
 		<groupId>it.polimi.dice</groupId>
 		<artifactId>it.polimi.dice.parent</artifactId>
-	<version>0.1.1-SNAPSHOT</version>
+	<version>0.2.0-SNAPSHOT</version>
 	</parent>
 </project>
diff --git a/plugin/it.polimi.dice.verification.feature/feature.xml b/plugin/it.polimi.dice.verification.feature/feature.xml
@@ -2,7 +2,7 @@
 <feature
       id="it.polimi.dice.verification.feature"
       label="DICE Verification"
-      version="0.1.1.qualifier">
+      version="0.2.0.qualifier">
 
    <description url="http://www.example.com/description">
       [Enter Feature Description here.]
@@ -20,7 +20,7 @@
          id="it.polimi.dice.verification"
          download-size="0"
          install-size="0"
-         version="0.1.1.qualifier"
+         version="0.2.0.qualifier"
          unpack="false"/>
 
    <plugin

diff --git a/plugin/it.polimi.dice.verification.feature/pom.xml b/plugin/it.polimi.dice.verification.feature/pom.xml
@@ -9,7 +9,7 @@
 	<parent>
 		<groupId>it.polimi.dice</groupId>
 		<artifactId>it.polimi.dice.parent</artifactId>
-	<version>0.1.1-SNAPSHOT</version>
+	<version>0.2.0-SNAPSHOT</version>
 	</parent>
 	<properties>
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

diff --git a/plugin/it.polimi.dice.verification.ui.feature/feature.xml b/plugin/it.polimi.dice.verification.ui.feature/feature.xml
@@ -2,7 +2,7 @@
 <feature
       id="it.polimi.dice.verification.ui.feature"
       label="DICE Verification UI"
-      version="0.1.1.qualifier">
+      version="0.2.0.qualifier">
 
    <description url="http://www.example.com/description">
       [Enter Feature Description here.]
@@ -20,7 +20,7 @@
          id="it.polimi.dice.verification.ui"
          download-size="0"
          install-size="0"
-         version="0.1.1.qualifier"
+         version="0.2.0.qualifier"
          unpack="false"/>
 
    <plugin

diff --git a/plugin/it.polimi.dice.verification.ui.feature/pom.xml b/plugin/it.polimi.dice.verification.ui.feature/pom.xml
@@ -9,7 +9,7 @@
 	<parent>
 		<groupId>it.polimi.dice</groupId>
 		<artifactId>it.polimi.dice.parent</artifactId>
-	<version>0.1.1-SNAPSHOT</version>
+	<version>0.2.0-SNAPSHOT</version>
 	</parent>
 	<properties>
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

diff --git a/plugin/it.polimi.dice.verification.ui/META-INF/MANIFEST.MF b/plugin/it.polimi.dice.verification.ui/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: DICE Verification UI
 Bundle-SymbolicName: it.polimi.dice.verification.ui;singleton:=true
-Bundle-Version: 0.1.1.qualifier
+Bundle-Version: 0.2.0.qualifier
 Bundle-Activator: it.polimi.dice.verification.ui.DiceVerificationUiPlugin
 Require-Bundle: org.eclipse.ui,
  org.eclipse.ui.ide,

diff --git a/plugin/it.polimi.dice.verification.ui/plugin.xml b/plugin/it.polimi.dice.verification.ui/plugin.xml
@@ -6,7 +6,7 @@
       <launchConfigurationTabGroup
             class="it.polimi.dice.verification.ui.launcher.VerificationLaunchConfigurationTabGroup"
             id="it.polimi.dice.verification.ui.launchConfigurationTabGroup"
-            type="it.polimi.dice.verification.launchConfigurationType">
+            type="it.polimi.dice.verification.launchConfigurationType1">
       </launchConfigurationTabGroup>
    </extension>
    <extension
@@ -21,7 +21,7 @@
    <extension
          point="org.eclipse.debug.ui.launchConfigurationTypeImages">
       <launchConfigurationTypeImage
-            configTypeID="it.polimi.dice.verification.launchConfigurationType"
+            configTypeID="it.polimi.dice.verification.launchConfigurationType1"
             icon="icons/verify_icon.png"
             id="it.polimi.dice.verification.ui.launchConfigurationTypeImage">
       </launchConfigurationTypeImage>
@@ -128,7 +128,7 @@
          </enablement>
  		</contextualLaunch>
        <configurationType
-              id="it.polimi.dice.verification.launchConfigurationType">
+              id="it.polimi.dice.verification.launchConfigurationType1">
        </configurationType>
        <description
               description="Launches a verification task on the specified UML model"

diff --git a/plugin/it.polimi.dice.verification.ui/pom.xml b/plugin/it.polimi.dice.verification.ui/pom.xml
@@ -9,7 +9,7 @@
 	<parent>
 		<groupId>it.polimi.dice</groupId>
 		<artifactId>it.polimi.dice.parent</artifactId>
-		<version>0.1.1-SNAPSHOT</version>
+		<version>0.2.0-SNAPSHOT</version>
 	</parent>
 	<properties>
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

diff --git a/...rification.ui/src/it/polimi/dice/verification/ui/launcher/MainLaunchConfigurationTab.java b/...rification.ui/src/it/polimi/dice/verification/ui/launcher/MainLaunchConfigurationTab.java
@@ -603,14 +603,6 @@ public void widgetSelected(SelectionEvent e) {
 				};
 			});
 
-			Button ae2zotButton = new Button(group, SWT.RADIO);
-			ae2zotButton.setText(Messages.MainLaunchConfigurationTab_ae2zotLabel);
-			ae2zotButton.addSelectionListener(new SelectionAdapter() {
-				public void widgetSelected(SelectionEvent e) {
-					data.getConfig().setZotPlugin(ZotPlugin.AE2ZOT);
-					setDirty(true);
-				};
-			});
 
 			if(data.getConfig().getZotPlugin()!=null){
 				switch (data.getConfig().getZotPlugin().getValue()) {
@@ -621,11 +613,7 @@ public void widgetSelected(SelectionEvent e) {
 				case ZotPlugin.AE2BVZOT_VALUE:
 					ae2bvzotButton.setSelection(true);
 					break;
-
-				case ZotPlugin.AE2ZOT_VALUE:
-					ae2zotButton.setSelection(true);
-					break;
-
+
 				default:
 					ae2sbvzotButton.setSelection(true);
 					break;

diff --git a/plugin/it.polimi.dice.verification.uml2json.feature/feature.xml b/plugin/it.polimi.dice.verification.uml2json.feature/feature.xml
@@ -2,7 +2,7 @@
 <feature
       id="it.polimi.dice.verification.uml2json.feature"
       label="DICE Uml2Json"
-      version="0.1.1.qualifier">
+      version="0.2.0.qualifier">
 
    <description url="http://www.example.com/description">
       [Enter Feature Description here.]

diff --git a/plugin/it.polimi.dice.verification.uml2json.feature/pom.xml b/plugin/it.polimi.dice.verification.uml2json.feature/pom.xml
@@ -9,7 +9,7 @@
 	<parent>
 		<groupId>it.polimi.dice</groupId>
 		<artifactId>it.polimi.dice.parent</artifactId>
-	<version>0.1.1-SNAPSHOT</version>
+	<version>0.2.0-SNAPSHOT</version>
 	</parent>
 	<properties>
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

diff --git a/plugin/it.polimi.dice.verification.uml2json/META-INF/MANIFEST.MF b/plugin/it.polimi.dice.verification.uml2json/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: Uml2json
 Bundle-SymbolicName: it.polimi.dice.verification.uml2json;singleton:=true
-Bundle-Version: 0.1.1.qualifier
+Bundle-Version: 0.2.0.qualifier
 Bundle-Activator: it.polimi.dice.verification.uml2json.Uml2JsonPlugin
 Require-Bundle: org.eclipse.core.runtime,
  org.eclipse.emf;bundle-version="2.6.0",

diff --git a/plugin/it.polimi.dice.verification.uml2json/pom.xml b/plugin/it.polimi.dice.verification.uml2json/pom.xml
@@ -9,7 +9,7 @@
 	<parent>
 		<groupId>it.polimi.dice</groupId>
 		<artifactId>it.polimi.dice.parent</artifactId>
-	<version>0.1.1-SNAPSHOT</version>
+	<version>0.2.0-SNAPSHOT</version>
 	</parent>
 	<properties>
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

diff --git a/plugin/it.polimi.dice.verification/META-INF/MANIFEST.MF b/plugin/it.polimi.dice.verification/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: Verification
 Bundle-SymbolicName: it.polimi.dice.verification;singleton:=true
-Bundle-Version: 0.1.1.qualifier
+Bundle-Version: 0.2.0.qualifier
 Bundle-Activator: it.polimi.dice.verification.DiceVerificationPlugin
 Require-Bundle: org.eclipse.core.runtime,
  it.polimi.dice.vtconfig,

diff --git a/plugin/it.polimi.dice.verification/plugin.xml b/plugin/it.polimi.dice.verification/plugin.xml
@@ -7,7 +7,7 @@
          point="org.eclipse.debug.core.launchConfigurationTypes">
       <launchConfigurationType
             delegate="it.polimi.dice.verification.launcher.VerificationLaunchConfigurationDelegate"
-            id="it.polimi.dice.verification.launchConfigurationType"
+            id="it.polimi.dice.verification.launchConfigurationType1"
             modes="run"
             name="DICE Verification">
       </launchConfigurationType>

diff --git a/plugin/it.polimi.dice.verification/pom.xml b/plugin/it.polimi.dice.verification/pom.xml
@@ -9,7 +9,7 @@
 	<parent>
 		<groupId>it.polimi.dice</groupId>
 		<artifactId>it.polimi.dice.parent</artifactId>
-	<version>0.1.1-SNAPSHOT</version>
+	<version>0.2.0-SNAPSHOT</version>
 	</parent>
 	<properties>
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

diff --git a/...n/it.polimi.dice.verification/src/it/polimi/dice/verification/DiceVerificationPlugin.java b/...n/it.polimi.dice.verification/src/it/polimi/dice/verification/DiceVerificationPlugin.java
@@ -7,7 +7,7 @@ public class DiceVerificationPlugin extends Plugin {
 
 	public static final String PLUGIN_ID = "it.polimi.dice.verification"; //$NON-NLS-1$
 
-	public static final String VERIFICATION_LAUNCH_CONFIGURATION_TYPE = "it.polimi.dice.verification.launchConfigurationType"; //$NON-NLS-1$
+	public static final String VERIFICATION_LAUNCH_CONFIGURATION_TYPE = "it.polimi.dice.verification.launchConfigurationType1"; //$NON-NLS-1$
 
 	private static DiceVerificationPlugin plugin;
 

diff --git a/plugin/it.polimi.dice.vtconfig/META-INF/MANIFEST.MF b/plugin/it.polimi.dice.vtconfig/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ Manifest-Version: 1.0
 Bundle-ManifestVersion: 2
 Bundle-Name: VtConfig
 Bundle-SymbolicName: it.polimi.dice.vtconfig;singleton:=true
-Bundle-Version: 0.1.1.qualifier
+Bundle-Version: 0.2.0.qualifier
 Bundle-RequiredExecutionEnvironment: JavaSE-1.8
 Require-Bundle: org.eclipse.emf.ecore,
  org.eclipse.core.runtime;bundle-version="3.11.1",

diff --git a/plugin/it.polimi.dice.vtconfig/pom.xml b/plugin/it.polimi.dice.vtconfig/pom.xml
@@ -9,7 +9,7 @@
 	<parent>
 		<groupId>it.polimi.dice</groupId>
 		<artifactId>it.polimi.dice.parent</artifactId>
-		<version>0.1.1-SNAPSHOT</version>
+		<version>0.2.0-SNAPSHOT</version>
 	</parent>
 	<properties>
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

diff --git a/plugin/pom.xml b/plugin/pom.xml
@@ -5,7 +5,7 @@
 
 	<groupId>it.polimi.dice</groupId>
 	<artifactId>it.polimi.dice.parent</artifactId>
-	<version>0.1.1-SNAPSHOT</version>
+	<version>0.2.0-SNAPSHOT</version>
 	<packaging>pom</packaging>
 
 	<name>it.polimi.dice.parent</name>