modelverse/services/LoLA/main.py

#!/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")