--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ebcsgen_pctl_parameter_synthesis.py	Fri Oct 07 12:37:22 2022 +0000
@@ -0,0 +1,50 @@
+import argparse
+
+from eBCSgen.Analysis.PCTL import PCTL
+from eBCSgen.Errors.FormulaParsingError import FormulaParsingError
+from eBCSgen.Errors.InvalidInputError import InvalidInputError
+from eBCSgen.Parsing.ParseBCSL import load_TS_from_json
+from eBCSgen.Parsing.ParsePCTLformula import PCTLparser
+
+
+args_parser = argparse.ArgumentParser(description='Parameter synthesis')
+
+args_parser._action_groups.pop()
+required = args_parser.add_argument_group('required arguments')
+optional = args_parser.add_argument_group('optional arguments')
+
+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('--region', type=str)
+
+args = args_parser.parse_args()
+
+if args.region:
+    region = args.region.replace("=", "<=")
+else:
+    region = None
+
+ts = load_TS_from_json(args.transition_file)
+
+if len(ts.params) == 0:
+    raise InvalidInputError("Provided model is not parametrised - parameter synthesis cannot be executed.")
+
+if "?" not in args.formula:
+    if not region:
+        params = set()
+    else:
+        params = {param.split("<=")[1] for param in region.split(",")}
+
+    undefined = set(ts.params) - params
+    if undefined:
+        raise InvalidInputError("Intervals undefined for parameters: {}.".format(", ".join(undefined)))
+
+formula = PCTLparser().parse(args.formula)
+if formula.success:
+    result = PCTL.parameter_synthesis(ts, formula, region)
+    f = open(args.output, "w")
+    f.write(result.decode("utf-8"))
+    f.close()
+else:
+    raise FormulaParsingError(formula.data, args.formula)