|
@@ -0,0 +1,40 @@
|
|
|
+#!/usr/bin/env python
|
|
|
+from modelverse import *
|
|
|
+from subprocess import Popen, PIPE
|
|
|
+import json
|
|
|
+
|
|
|
+init(address)
|
|
|
+login("test_service", "my_password")
|
|
|
+
|
|
|
+def lola_service(port):
|
|
|
+ json_input = service_get(port)
|
|
|
+ input_data = json.loads(json_input)
|
|
|
+ print input_data['petrinet']
|
|
|
+ print input_data['query']
|
|
|
+ query_formula = "--formula=EF ("+ input_data['query']+")"
|
|
|
+ lola = Popen(["lola", "--path=path_output", query_formula, "--json=output.json"], stdin=PIPE, stdout=PIPE).communicate(input=input_data['petrinet'])
|
|
|
+
|
|
|
+ output_file = open('output.json', 'r')
|
|
|
+ result = json.load(output_file)
|
|
|
+ output_file.close()
|
|
|
+ # If safety query is violated resulting True in output
|
|
|
+ path = ''
|
|
|
+ if result['analysis']['result']:
|
|
|
+ with open('path_output') as f:
|
|
|
+ for transition in f:
|
|
|
+ transition = transition.replace('\n',',')
|
|
|
+ path = path + transition
|
|
|
+ #json_result = '{"analysis_result": True , "path":\"'+path.rstrip(',') + '\"}'
|
|
|
+ service_set(port, result['analysis']['result'])
|
|
|
+ service_set(port, path.rstrip(','))
|
|
|
+
|
|
|
+service_register("lola", lola_service)
|
|
|
+print("Registered")
|
|
|
+
|
|
|
+while raw_input() != "STOP":
|
|
|
+ # Stay active, as we shouldn't exit while the service is running!
|
|
|
+ pass
|
|
|
+print("Stopping")
|
|
|
+
|
|
|
+service_stop()
|
|
|
+print("Service halted")
|