analyze_LoLA.py 1.1 KB

123456789101112131415161718192021
  1. import sys
  2. sys.path.append("wrappers/")
  3. from modelverse import *
  4. init()
  5. login("admin", "admin")
  6. model_add("formalisms/PetriNets", "formalisms/SimpleClassDiagrams", open("models/PetriNets/metamodels/PetriNets.mvc", 'r').read())
  7. model_add("formalisms/Query", "formalisms/SimpleClassDiagrams", open("models/SafetyQuery/metamodels/query.mvc", 'r').read())
  8. model_add("formalisms/PNPath", "formalisms/SimpleClassDiagrams", open("models/PNPath/metamodels/PNPath.mvc", 'r').read())
  9. model_add("models/PN", "formalisms/PetriNets", open("models/PetriNets/models/critical_section_with_check.mvc", 'r').read())
  10. model_add("models/Query", "formalisms/Query", open("models/SafetyQuery/models/both_criticals_enabled.mvc", 'r').read())
  11. transformation_add_AL({"PN": "formalisms/PetriNets", "Query": "formalisms/Query"}, {"Path": "formalisms/PNPath"}, "models/analyze_lola", open("models/PetriNets/transformations/analyze_lola.alc", 'r').read())
  12. if transformation_execute_AL("models/analyze_lola", {"PN": "models/PN", "Query": "models/Query"}, {"Path": "models/Path"}):
  13. print("Not reachable!")
  14. else:
  15. print("Reachable: " + str(element_list_nice("models/Path")))