Merge pull request #63 from sybila/update_storm_call

Remove remote Storm calls

Galaxy/tools/PCTLModelChecking/PCTLModelChecking.py

@@ -10,7 +10,6 @@
 usage: PCTLModelChecking.py [-h] --transition_file TRANSITION_FILE 
                                  --output OUTPUT 
                                  --formula FORMULA 
-                                 [--local_storm]
 
 Model checking
 
@@ -19,8 +18,6 @@
   --output OUTPUT
   --formula FORMULA
 
-optional arguments:
-  --local_storm
 """
 
 args_parser = argparse.ArgumentParser(description='Model checking')
@@ -32,15 +29,9 @@
 required.add_argument('--transition_file', required=True)
 required.add_argument('--output', type=str, required=True)
 required.add_argument('--formula', type=str, required=True)
-optional.add_argument('--local_storm', nargs="?", const=True)
 
 args = args_parser.parse_args()
 
-if args.local_storm:
-    local_storm = True
-else:
-    local_storm = False
-
 ts = load_TS_from_json(args.transition_file)
 # TODO for presence of rates
 
@@ -49,7 +40,7 @@
 
 formula = PCTLparser().parse(args.formula)
 if formula.success:
-    result = PCTL.model_checking(ts, formula, storm_local=local_storm)
+    result = PCTL.model_checking(ts, formula)
     f = open(args.output, "w")
     f.write(result.decode("utf-8"))
     f.close()

Galaxy/tools/PCTLParameterSynthesis/PCTLParameterSynthesis.py

@@ -10,8 +10,7 @@
 usage: PCTLParameterSynthesis.py [-h] --transition_file TRANSITION_FILE 
                                       --output OUTPUT 
                                       --formula FORMULA
-                                      [--region REGION] 
-                                      [--local_storm]                        
+                                      [--region REGION]               
 
 Parameter synthesis
 
@@ -22,7 +21,6 @@
 
 optional arguments:
   --region REGION
-  --local_storm
 """
 
 args_parser = argparse.ArgumentParser(description='Parameter synthesis')
@@ -34,7 +32,6 @@
 required.add_argument('--transition_file', required=True)
 required.add_argument('--output', type=str, required=True)
 required.add_argument('--formula', type=str, required=True)
-optional.add_argument('--local_storm', nargs="?", const=True)
 optional.add_argument('--region', type=str)
 
 args = args_parser.parse_args()
@@ -44,11 +41,6 @@
 else:
     region = None
 
-if args.local_storm:
-    local_storm = True
-else:
-    local_storm = False
-
 ts = load_TS_from_json(args.transition_file)
 # TODO for presence of rates
 
@@ -67,7 +59,7 @@
 
 formula = PCTLparser().parse(args.formula)
 if formula.success:
-    result = PCTL().parameter_synthesis(ts, formula, region, local_storm)
+    result = PCTL().parameter_synthesis(ts, formula, region)
     f = open(args.output, "w")
     f.write(result.decode("utf-8"))
     f.close()

eBCSgen/Analysis/PCTL.py

@@ -7,7 +7,7 @@
 
 class PCTL:
     @staticmethod
-    def model_checking(ts: TransitionSystem, PCTL_formula: Formula, storm_local: bool = True):
+    def model_checking(ts: TransitionSystem, PCTL_formula: Formula):
         """
         Model checking of given PCTL formula.
 
@@ -17,7 +17,6 @@ def model_checking(ts: TransitionSystem, PCTL_formula: Formula, storm_local: boo
 
         :param ts: given transition system
         :param PCTL_formula: given PCTL formula
-        :param storm_local: use local Storm installation
         :return: output of Storm model checker
         """
         path = "/tmp/"
@@ -30,12 +29,11 @@ def model_checking(ts: TransitionSystem, PCTL_formula: Formula, storm_local: boo
         ts.save_to_STORM_explicit(transitions_file, labels_file, state_labels, AP_labels)
 
         command = "storm --explicit {0} {1} --prop '{2}'"
-        result = call_storm(command.format(transitions_file, labels_file, formula),
-                            [transitions_file, labels_file], storm_local)
+        result = call_storm(command.format(transitions_file, labels_file, formula))
         return result
 
     @staticmethod
-    def parameter_synthesis(ts: TransitionSystem, PCTL_formula: Formula, region: str, storm_local: bool = True):
+    def parameter_synthesis(ts: TransitionSystem, PCTL_formula: Formula, region: str):
         """
         Parameter synthesis of given PCTL formula in given region.
 
@@ -46,7 +44,6 @@ def parameter_synthesis(ts: TransitionSystem, PCTL_formula: Formula, region: str
         :param ts: given transition system
         :param PCTL_formula: given PCTL formula
         :param region: string representation of region which will be checked by Storm
-        :param storm_local: use local Storm installation
         :return: output of Storm model checker
         """
         path = "/tmp/"
@@ -62,50 +59,13 @@ def parameter_synthesis(ts: TransitionSystem, PCTL_formula: Formula, region: str
         command_no_region = "storm-pars --prism {0} --prop '{1}'"
 
         if region:
-            result = call_storm(command_region.format(prism_file, formula, region), [prism_file], storm_local)
+            result = call_storm(command_region.format(prism_file, formula, region))
         else:
-            result = call_storm(command_no_region.format(prism_file, formula), [prism_file], storm_local)
+            result = call_storm(command_no_region.format(prism_file, formula))
         return result
 
 
-def call_storm(command: str, files: list, storm_local: bool):
-    """
-    Calls Storm model checker either locally or on the remote server.
-
-    :param command: given command to be executed
-    :param files: files to be transferred to remote device
-    :param storm_local: use local Storm installation
-    :return: result of Storm execution
-    """
-    if storm_local:
-        return call_local_storm(command)
-    else:
-        import paramiko, scp
-        ssh = paramiko.SSHClient()
-        ssh.load_system_host_keys()
-        try:
-            ssh.connect("psyche07.fi.muni.cz", username="biodivine")
-        except Exception:
-            return call_local_storm(command)
-
-        with scp.SCPClient(ssh.get_transport()) as tunnel:
-            for file in files:
-                tunnel.put(file, file)
-
-        ssh_stdin, ssh_stdout, ssh_stderr = ssh.exec_command(command)
-        output = ssh_stdout.read()
-        stderr = ssh_stderr.read()
-        ssh.close()
-        del ssh, ssh_stdin, ssh_stdout, ssh_stderr
-
-        # if error output is empty, command was executed successfully, call local Storm otherwise
-        if stderr:
-            return call_local_storm(command)
-        else:
-            return output
-
-
-def call_local_storm(command: str):
+def call_storm(command: str):
     """
     Calls Storm model checker locally.