Merge pull request #23 from sybila/galaxy-config-ctl

Galaxy config ctl

TS/State.py

@@ -124,7 +124,7 @@ def to_PRISM_string(self, apostrophe=False) -> str:
         :return: PRISM string representation
         """
         aps = "'" if apostrophe else ""
-        vars = list(map(lambda i: f'(VAR_{i}{aps}={int(self.sequence[i])})', range(len(self))))
+        vars = list(map(lambda i: '(VAR_{}{}={})'.format(i, aps, int(self.sequence[i])), range(len(self))))
         return " & ".join(vars)
 
 

TS/TransitionSystem.py

@@ -210,7 +210,7 @@ def save_to_prism(self, output_file: str, params: set, prism_formulas: list):
 
         # declare state variables
         init = decoding[self.init]
-        vars = [f'\tVAR_{i} : [0..{ self.bound + 1}] init {int(init.sequence[i])}; // {self.ordering[i]}'
+        vars = ['\tVAR_{} : [0..{}] init {}; // {}'.format(i, self.bound + 1, int(init.sequence[i]), self.ordering[i])
                 for i in range(len(self.ordering))]
         prism_file.write("\n" + "\n".join(vars) + "\n")
 
@@ -235,7 +235,7 @@ def edges_to_PRISM(self, decoding):
         output = []
         for group in self:
             source = group[0].source
-            line = f'\t[] {decoding[source].to_PRISM_string()} -> ' + \
+            line = '\t[] {} -> '.format(decoding[source].to_PRISM_string()) + \
                    " + ".join(list(map(lambda edge: edge.to_PRISM_string(decoding), group))) + ";"
             output.append(line)
         return output

config/datatypes/datatypes.py

@@ -109,3 +109,27 @@ def set_peek(self, dataset, is_multi_byte=False):
             dataset.peek = 'file does not exist'
             dataset.blurb = 'file purged from disk'
 
+class CTL_check(Text):
+    """Class describing a CTL model checking output"""
+    file_ext = "ctl.check"
+
+    def sniff(self, filename):
+        """
+        Determines whether the file is in .ctl.check format
+        """
+        content = open(filename, 'r').read()
+        keywords = ["Result:", "Number of satisfying states:"]
+        return all(keyword in content for keyword in keywords)
+
+    def set_peek(self, dataset, is_multi_byte=False):
+        if not dataset.dataset.purged:
+            result = open(dataset.file_name, "r")
+            answer = ""
+            for line in result.readlines():
+                if "Result:" in line:
+                    answer = line.split()[-1]
+            dataset.peek = "Model checking result: {}".format(answer)
+            dataset.blurb = nice_size(dataset.get_size())
+        else:
+            dataset.peek = 'file does not exist'
+            dataset.blurb = 'file purged from disk'

config/eBCSgen_CTLmodelChecking.xml

@@ -0,0 +1,26 @@
+<tool id="CTLModelChecking" name="CTL Model Checking" version="1.1.0">
+  <description> - explicit CTL model checking of given model</description>
+    <options sanitize="False"/>
+    <command>python3 /home/xtrojak/eBCSgen/Callables/CTLModelChecking.py
+      --transition_file '$transition_file'
+      --output '$output'
+      --formula '$formula'
+  </command>
+
+  <inputs>
+    <param format="bcs.ts" name="transition_file" type="data" label="Computed Transition system"/>
+    <param name="formula" type="text" label="PCTL formula">
+      <validator type="empty_field"/>
+    </param>
+  </inputs>
+
+  <outputs>
+    <data format="ctl.check" name="output" />
+  </outputs>
+
+  <tests>
+    <test>
+    </test>
+  </tests>
+
+</tool>

config/eBCSgen_modelChecking.xml → config/eBCSgen_PCTLmodelChecking.xml

@@ -1,21 +1,17 @@
-<tool id="ModelChecking" name="PCTL Model Checking" version="1.0.0">
+<tool id="ModelChecking" name="PCTL Model Checking" version="1.1.0">
   <description> - explicit PCTL model checking of given model</description>
     <options sanitize="False"/>
-    <command>python3 /home/xtrojak/eBCSgen/Callables/ModelChecking.py
-      --model '$model'
+    <command>python3 /home/xtrojak/eBCSgen/Callables/PCTLModelChecking.py
+      --transition_file '$transition_file'
       --output '$output'
       --formula '$formula'
-      #if $bound != "":
-          --bound '$bound'
-      #end if
   </command>
 
   <inputs>
-    <param format="bcs" name="model" type="data" label="Model file" help="Provide a .bcs file"/>
+    <param format="bcs.ts" name="transition_file" type="data" label="Computed Transition system"/>
     <param name="formula" type="text" label="PCTL formula">
       <validator type="empty_field"/>
     </param>
-    <param name="bound" min="0" type="integer" value="" label="Bound [optional]" optional="true"/>
   </inputs>
 
   <outputs>

config/eBCSgen_parameterSynthesis.xml → config/eBCSgen_PCTLparameterSynthesis.xml

@@ -1,31 +1,26 @@
-<tool id="ParameterSynthesis" name="PCTL Parameter Synthesis" version="1.0.0">
+<tool id="ParameterSynthesis" name="PCTL Parameter Synthesis" version="1.1.0">
   <description> - PCTL parameter synthesis of given model</description>
     <options sanitize="False"/>
-    <command>python3 /home/xtrojak/eBCSgen/Callables/ParameterSynthesis.py
-      --model '$model'
+    <command>python3 /home/xtrojak/eBCSgen/Callables/PCTLParameterSynthesis.py
+      --transition_file '$transition_file'
       #if len($regions) > 0:
           --output '$output_regions'
       #else:
           --output '$output_sample'
       #end if
       --formula '$formula'
 
-      #if $bound != "":
-          --bound '$bound'
-      #end if
-
       #set parameters = ",".join([str($s.from) + "=" + str($s.param) + "=" + str($s.to) for $s in $regions])
       #if $parameters:
           --region '$parameters'
       #end if
   </command>
 
   <inputs>
-    <param format="bcs" name="model" type="data" label="Model file" help="Provide a .bcs file"/>
+    <param format="bcs.ts" name="transition_file" type="data" label="Computed Transition system"/>
     <param name="formula" type="text" label="PCTL formula">
        <validator type="empty_field"/>
     </param>
-    <param name="bound" size="4" type="integer" value="" label="Bound [optional]" optional="true"/>
 
     <repeat name="regions" title="Intervals">
         <param name="param" value="" type="text" label="Parameter:">

config/tours/PCTL-Model-Checking.yaml

@@ -13,29 +13,25 @@ steps:
   - title: Step 2 - Select tool
     element: >-
       #left > div.unified-panel > div.unified-panel-body > div > div.toolMenu >
-      div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(3) > a >
+      div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(4) > a >
       span.description
     content: "Click on PCTL Model Checking tool."
     placement: bottom
-  - title: Step 3 - Model file
-    element: 'div[tour_id="model"]'
+  - title: Step 3 - Computed Transition system
+    element: 'div[tour_id="transition_file"]'
     content:
-      "Choose BCSL model file. <br>
-      This tool supports only .bcs files stored in your history."
+      "You can choose a precomputed Transition System file. <br>
+      This tool supports only .bcs.ts files stored in your history."
     placement: auto
   - title: Step 4 - PCTL Formula
     element: 'div[tour_id="formula"]'
     content: "Enter PCTL formula."
     placement: auto
-  - title: Step 5 - Bound
-    element: 'div[tour_id="bound"]'
-    content: "Specify agents boundary cap (optional)."
-    placement: auto
-  - title: Step 6 - Execute
+  - title: Step 5 - Execute
     element: '#execute'
     content: "Click the button Execute <br>to start model checking."
     placement: auto
-  - title: Step 7 - Results
+  - title: Step 6 - Results
     element: .list-items
     content:
       "Wait until the model checking is finished<br>

config/tours/PCTL-Parameter-Synthesis.yaml

@@ -13,51 +13,46 @@ steps:
   - title: Step 2 - Select tool
     element: >-
       #left > div.unified-panel > div.unified-panel-body > div > div.toolMenu >
-      div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(4) > a
+      div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(5) > a
     content: "Click on PCTL Parameter Synthesis tool."
     placement: bottom
-  - title: Step 3 - Model file
-    element: 'div[tour_id="model"]'
+  - title: Step 3 - Computed Transition system
+    element: 'div[tour_id="transition_file"]'
     content:
-      "Choose BCSL model file. <br>
-      This tool supports only .bcs files stored in your history."
-    placement: auto
+      "You can choose a precomputed Transition System file. <br>
+      This tool supports only .bcs.ts files stored in your history."
   - title: Step 4 - PCTL Formula
     element: 'div[tour_id="formula"]'
     content: "Enter PCTL formula."
     placement: auto
-  - title: Step 5 - Bound
-    element: 'div[tour_id="bound"]'
-    content: "Specify agents boundary cap (optional)."
-    placement: auto
-  - title: Step 6 - Insert Interval
+  - title: Step 5 - Insert Interval
     element: '#center .center-container .center-panel .ui-portlet .portlet-content .portlet-body
     .ui-form-element .ui-form-field button .ui-button-default.btn.btn-secondary.float-none.form-repeat-add'
     content:
       "Please specify values interval for<br>
       each unknown parameter."
     placement: auto
-  - title: Step 7 - Parameter name
+  - title: Step 6 - Parameter name
     element: 'div[tour_id="regions_0|param"]'
     content: "Enter parameter name."
     placement: bottom
-  - title: Step 8 - Parameter interval start
+  - title: Step 7 - Parameter interval start
     element: 'div[tour_id="regions_0|from"]'
     content: "Enter start of the interval."
     placement: bottom
-  - title: Step 9 - Parameter interval end
+  - title: Step 8 - Parameter interval end
     element: 'div[tour_id="regions_0|to"]'
     content: "Enter end of the interval."
     placement: bottom
-  - title: Step 10 - Delete Interval
+  - title: Step 9 - Delete Interval
     element: '#button_delete'
     content: "Option to delete your interval."
     placement: left
-  - title: Step 11 - Execute
+  - title: Step 10 - Execute
     element: '#execute'
     content: "Click the button Execute <br>to start parameter synthesis."
     placement: auto
-  - title: Step 12 - Results
+  - title: Step 11 - Results
     element: .list-items
     content:
       "Wait until the parameter synthesis is <br>

config/tours/Probability-Sampling.yaml

@@ -13,7 +13,7 @@ steps:
   - title: Step 2 - Select tool
     element: >-
       #left > div.unified-panel > div.unified-panel-body > div > div.toolMenu >
-      div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(6) > a
+      div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(7) > a
     content: "Click on Probability Sampling tool."
     placement: bottom
   - title: Step 3 - Storm output file

config/tours/SA-Context-Based-Reduction.yaml

@@ -15,7 +15,7 @@ steps:
   - title: Step 2 - Select tool
     element: >-
       #left > div.unified-panel > div.unified-panel-body > div > div.toolMenu >
-      div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(5) > a
+      div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(6) > a
     content: "Click on Static Analysis tool."
     placement: bottom
   - title: Step 3 - Model file

config/tours/SA-non-reachibility.yaml

@@ -15,7 +15,7 @@ steps:
   - title: Step 2 - Select tool
     element: >-
       #left > div.unified-panel > div.unified-panel-body > div > div.toolMenu >
-      div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(5) > a
+      div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(6) > a
     content: "Click on Static Analysis tool."
     placement: bottom
   - title: Step 3 - Model file

config/tours/SA-redundandancy-Elimination.yaml

@@ -15,7 +15,7 @@ steps:
   - title: Step 2 - Select tool
     element: >-
       #left > div.unified-panel > div.unified-panel-body > div > div.toolMenu >
-      div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(5) > a
+      div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(6) > a
     content: "Click on Static Analysis tool."
     placement: bottom
   - title: Step 3 - Model file