modelverse/services/LoLA/main.py

#!/usr/bin/env python
import sys
import os
sys.path.append("wrappers")

from modelverse import *
from subprocess import Popen, PIPE
import json

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(["services/LoLA/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(','))

    os.remove("path_output")
    os.remove("output.json")

try:
    init(sys.argv[1])
    login("LoLA", "LoLA_password")

    service_register("lola", lola_service)

    try:
        if sys.version_info[0] < 3:
            while raw_input() != "STOP":
                # Stay active, as we shouldn't exit while the service is running!
                pass
        else:
            while input() != "STOP":
                # Stay active, as we shouldn't exit while the service is running!
                pass

    finally:
        service_stop()
except KeyboardInterrupt:
    pass