diff --git a/api/ebcsgen_ctl_model_checking.py b/api/ebcsgen_ctl_model_checking.py new file mode 100644 index 0000000..74c8cfe --- /dev/null +++ b/api/ebcsgen_ctl_model_checking.py @@ -0,0 +1,33 @@ +import argparse + +from eBCSgen.Analysis.CTL import CTL +from eBCSgen.Errors.FormulaParsingError import FormulaParsingError +from eBCSgen.Errors.InvalidInputError import InvalidInputError +from eBCSgen.Parsing.ParseBCSL import load_TS_from_json +from eBCSgen.Parsing.ParseCTLformula import CTLparser + +args_parser = argparse.ArgumentParser(description='Model checking') + +args_parser._action_groups.pop() +required = args_parser.add_argument_group('required arguments') + +required.add_argument('--transition_file', required=True) +required.add_argument('--output', type=str, required=True) +required.add_argument('--formula', type=str, required=True) + +args = args_parser.parse_args() + +ts = load_TS_from_json(args.transition_file) + +if len(ts.params) != 0: + raise InvalidInputError("Provided transition system is parametrised - model checking cannot be executed.") + +formula = CTLparser().parse(args.formula) +if formula.success: + result, states = CTL.model_checking(ts, formula) + output = 'Result: {}\nNumber of satisfying states: {}'.format(result, len(states)) + f = open(args.output, "w") + f.write(output) + f.close() +else: + raise FormulaParsingError(formula.data, args.formula) diff --git a/api/ebcsgen_generate_ts.py b/api/ebcsgen_generate_ts.py new file mode 100644 index 0000000..55ee60a --- /dev/null +++ b/api/ebcsgen_generate_ts.py @@ -0,0 +1,43 @@ +import argparse + +from eBCSgen.Errors.ModelParsingError import ModelParsingError +from eBCSgen.Errors.UnspecifiedParsingError import UnspecifiedParsingError +from eBCSgen.Parsing.ParseBCSL import Parser + +import numpy as np + + +args_parser = argparse.ArgumentParser(description='Transition system generating') + +args_parser._action_groups.pop() +required = args_parser.add_argument_group('required arguments') +optional = args_parser.add_argument_group('optional arguments') + +required.add_argument('--model', type=str, required=True) +required.add_argument('--output', type=str, required=True) +required.add_argument('--direct', required=True) + +optional.add_argument('--max_time', type=float, default=np.inf) +optional.add_argument('--max_size', type=float, default=np.inf) +optional.add_argument('--bound', type=int, default=None) + +args = args_parser.parse_args() + +model_parser = Parser("model") +model_str = open(args.model, "r").read() + +model = model_parser.parse(model_str) +if model.success: + if eval(args.direct): + ts = model.data.generate_direct_transition_system(args.max_time, + args.max_size, + args.bound) + ts.change_to_vector_backend() + else: + vm = model.data.to_vector_model(args.bound) + ts = vm.generate_transition_system(None, args.max_time, args.max_size) + ts.save_to_json(args.output, model.data.params) +else: + if "error" in model.data: + raise UnspecifiedParsingError(model.data["error"]) + raise ModelParsingError(model.data, model_str) diff --git a/api/ebcsgen_pctl_model_checking.py b/api/ebcsgen_pctl_model_checking.py new file mode 100644 index 0000000..66629bf --- /dev/null +++ b/api/ebcsgen_pctl_model_checking.py @@ -0,0 +1,33 @@ +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='Model checking') + +args_parser._action_groups.pop() +required = args_parser.add_argument_group('required arguments') + +required.add_argument('--transition_file', required=True) +required.add_argument('--output', type=str, required=True) +required.add_argument('--formula', type=str, required=True) + +args = args_parser.parse_args() + +ts = load_TS_from_json(args.transition_file) + +if len(ts.params) != 0: + raise InvalidInputError("Provided transition system is parametrised - model checking cannot be executed.") + +formula = PCTLparser().parse(args.formula) +if formula.success: + result = PCTL.model_checking(ts, formula) + f = open(args.output, "w") + f.write(result.decode("utf-8")) + f.close() +else: + raise FormulaParsingError(formula.data, args.formula) diff --git a/api/ebcsgen_pctl_parameter_synthesis.py b/api/ebcsgen_pctl_parameter_synthesis.py new file mode 100644 index 0000000..0996d78 --- /dev/null +++ b/api/ebcsgen_pctl_parameter_synthesis.py @@ -0,0 +1,62 @@ +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 + + +class FakeFile: + def __init__(self, content): + self.content = content.decode("utf-8") + + def read(self): + return self.content + + +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) + if "?" not in args.formula: + result = FakeFile(result) + df = PCTL.process_output(result) + df.to_csv(args.output, index=False) + else: + with open(args.output, "w") as f: + f.write(result.decode("utf-8")) +else: + raise FormulaParsingError(formula.data, args.formula) diff --git a/api/ebcsgen_sbml_export.py b/api/ebcsgen_sbml_export.py new file mode 100644 index 0000000..a7639d8 --- /dev/null +++ b/api/ebcsgen_sbml_export.py @@ -0,0 +1,30 @@ +import argparse + +from eBCSgen.Errors.ModelParsingError import ModelParsingError +from eBCSgen.Errors.UnspecifiedParsingError import UnspecifiedParsingError +from eBCSgen.Parsing.ParseBCSL import Parser + +import libsbml + + +args_parser = argparse.ArgumentParser(description='Export SBML model with usage of SBML-multi package') + +args_parser._action_groups.pop() +required = args_parser.add_argument_group('required arguments') + +required.add_argument('--model', type=str, required=True) +required.add_argument('--output', type=str, required=True) + +args = args_parser.parse_args() + +model_parser = Parser("model") +model_str = open(args.model, "r").read() + +model = model_parser.parse(model_str) +if model.success: + document = model.data.export_sbml() + libsbml.writeSBMLToFile(document, args.output) +else: + if "error" in model.data: + raise UnspecifiedParsingError(model.data["error"]) + raise ModelParsingError(model.data, model_str) diff --git a/api/ebcsgen_simulate.py b/api/ebcsgen_simulate.py new file mode 100644 index 0000000..bb42ac3 --- /dev/null +++ b/api/ebcsgen_simulate.py @@ -0,0 +1,51 @@ +import argparse + +from eBCSgen.Errors import UnspecifiedParsingError +from eBCSgen.Errors.InvalidInputError import InvalidInputError +from eBCSgen.Errors.ModelParsingError import ModelParsingError +from eBCSgen.Errors.RatesNotSpecifiedError import RatesNotSpecifiedError +from eBCSgen.Parsing.ParseBCSL import Parser + + +args_parser = argparse.ArgumentParser(description='Simulation') + +args_parser._action_groups.pop() +required = args_parser.add_argument_group('required arguments') + +required.add_argument('--model', type=str, required=True) +required.add_argument('--output', type=str, required=True) +required.add_argument('--deterministic', required=True) +required.add_argument('--direct', required=True) +required.add_argument('--runs', type=int, required=True) +required.add_argument('--max_time', type=float, required=True) +required.add_argument('--volume', type=float, required=True) +required.add_argument('--step', type=float, required=True) + +args = args_parser.parse_args() + +model_parser = Parser("model") +model_str = open(args.model, "r").read() + +model = model_parser.parse(model_str) + +if model.success: + if len(model.data.params) != 0: + raise InvalidInputError("Provided model is parametrised - simulation cannot be executed.") + if not model.data.all_rates: + raise RatesNotSpecifiedError("Some rules do not have rates specified - simulation cannot be executed.") + + if eval(args.deterministic): + vm = model.data.to_vector_model() + df = vm.deterministic_simulation(args.max_time, args.volume, args.step) + else: + if eval(args.direct): + df = model.data.network_free_simulation(args.max_time) + else: + vm = model.data.to_vector_model() + df = vm.stochastic_simulation(args.max_time, args.runs) + + df.to_csv(args.output, index=None, header=True) +else: + if "error" in model.data: + raise UnspecifiedParsingError(model.data["error"]) + raise ModelParsingError(model.data, model_str) diff --git a/api/ebcsgen_static_analysis.py b/api/ebcsgen_static_analysis.py new file mode 100644 index 0000000..2425ddf --- /dev/null +++ b/api/ebcsgen_static_analysis.py @@ -0,0 +1,54 @@ +import argparse + +from eBCSgen.Errors.ComplexParsingError import ComplexParsingError +from eBCSgen.Errors.ModelParsingError import ModelParsingError +from eBCSgen.Errors.UnspecifiedParsingError import UnspecifiedParsingError +from eBCSgen.Parsing.ParseBCSL import Parser + + +def save_model(model, filename): + f = open(filename, "w") + f.write(repr(model)) + f.close() + + +args_parser = argparse.ArgumentParser(description='Static analysis') + +args_parser._action_groups.pop() +required = args_parser.add_argument_group('required arguments') +optional = args_parser.add_argument_group('optional arguments') + +required.add_argument('--model', type=str, required=True) +required.add_argument('--output', type=str, required=True) +required.add_argument('--method', type=str, required=True) +optional.add_argument('--complex') + +args = args_parser.parse_args() + +model_parser = Parser("model") +model_str = open(args.model, "r").read() +model = model_parser.parse(model_str) + +if model.success: + if args.method == "reduce": + model.data.reduce_context() + save_model(model.data, args.output) + elif args.method == "eliminate": + model.data.eliminate_redundant() + save_model(model.data, args.output) + else: + complex_parser = Parser("rate_complex") + complex = complex_parser.parse(args.complex) + if complex.success: + result = model.data.static_non_reachability(complex.data.children[0]) + f = open(args.output, "w") + s = "can possibly" if result else "cannot" + message = "The given agent\n\t{}\n{} be reached in the model.".format(complex.data.children[0], s) + f.write(message) + f.close() + else: + raise ComplexParsingError(complex.data, args.complex) +else: + if "error" in model.data: + raise UnspecifiedParsingError(model.data["error"]) + raise ModelParsingError(model.data, model_str)