diff --git a/TS/State.py b/TS/State.py index 2687039..f1bba10 100644 --- a/TS/State.py +++ b/TS/State.py @@ -124,7 +124,7 @@ def to_PRISM_string(self, apostrophe=False) -> str: :return: PRISM string representation """ aps = "'" if apostrophe else "" - vars = list(map(lambda i: f'(VAR_{i}{aps}={int(self.sequence[i])})', range(len(self)))) + vars = list(map(lambda i: '(VAR_{}{}={})'.format(i, aps, int(self.sequence[i])), range(len(self)))) return " & ".join(vars) diff --git a/TS/TransitionSystem.py b/TS/TransitionSystem.py index 9297d19..5a3ef90 100644 --- a/TS/TransitionSystem.py +++ b/TS/TransitionSystem.py @@ -210,7 +210,7 @@ def save_to_prism(self, output_file: str, params: set, prism_formulas: list): # declare state variables init = decoding[self.init] - vars = [f'\tVAR_{i} : [0..{ self.bound + 1}] init {int(init.sequence[i])}; // {self.ordering[i]}' + vars = ['\tVAR_{} : [0..{}] init {}; // {}'.format(i, self.bound + 1, int(init.sequence[i]), self.ordering[i]) for i in range(len(self.ordering))] prism_file.write("\n" + "\n".join(vars) + "\n") @@ -235,7 +235,7 @@ def edges_to_PRISM(self, decoding): output = [] for group in self: source = group[0].source - line = f'\t[] {decoding[source].to_PRISM_string()} -> ' + \ + line = '\t[] {} -> '.format(decoding[source].to_PRISM_string()) + \ " + ".join(list(map(lambda edge: edge.to_PRISM_string(decoding), group))) + ";" output.append(line) return output diff --git a/config/datatypes/datatypes.py b/config/datatypes/datatypes.py index d606013..baa0203 100644 --- a/config/datatypes/datatypes.py +++ b/config/datatypes/datatypes.py @@ -109,3 +109,27 @@ def set_peek(self, dataset, is_multi_byte=False): dataset.peek = 'file does not exist' dataset.blurb = 'file purged from disk' +class CTL_check(Text): + """Class describing a CTL model checking output""" + file_ext = "ctl.check" + + def sniff(self, filename): + """ + Determines whether the file is in .ctl.check format + """ + content = open(filename, 'r').read() + keywords = ["Result:", "Number of satisfying states:"] + return all(keyword in content for keyword in keywords) + + def set_peek(self, dataset, is_multi_byte=False): + if not dataset.dataset.purged: + result = open(dataset.file_name, "r") + answer = "" + for line in result.readlines(): + if "Result:" in line: + answer = line.split()[-1] + dataset.peek = "Model checking result: {}".format(answer) + dataset.blurb = nice_size(dataset.get_size()) + else: + dataset.peek = 'file does not exist' + dataset.blurb = 'file purged from disk' diff --git a/config/eBCSgen_CTLmodelChecking.xml b/config/eBCSgen_CTLmodelChecking.xml new file mode 100644 index 0000000..94a1761 --- /dev/null +++ b/config/eBCSgen_CTLmodelChecking.xml @@ -0,0 +1,26 @@ + + - explicit CTL model checking of given model + + python3 /home/xtrojak/eBCSgen/Callables/CTLModelChecking.py + --transition_file '$transition_file' + --output '$output' + --formula '$formula' + + + + + + + + + + + + + + + + + + + diff --git a/config/eBCSgen_modelChecking.xml b/config/eBCSgen_PCTLmodelChecking.xml similarity index 51% rename from config/eBCSgen_modelChecking.xml rename to config/eBCSgen_PCTLmodelChecking.xml index 830037b..ee80b8a 100644 --- a/config/eBCSgen_modelChecking.xml +++ b/config/eBCSgen_PCTLmodelChecking.xml @@ -1,21 +1,17 @@ - + - explicit PCTL model checking of given model - python3 /home/xtrojak/eBCSgen/Callables/ModelChecking.py - --model '$model' + python3 /home/xtrojak/eBCSgen/Callables/PCTLModelChecking.py + --transition_file '$transition_file' --output '$output' --formula '$formula' - #if $bound != "": - --bound '$bound' - #end if - + - diff --git a/config/eBCSgen_parameterSynthesis.xml b/config/eBCSgen_PCTLparameterSynthesis.xml similarity index 77% rename from config/eBCSgen_parameterSynthesis.xml rename to config/eBCSgen_PCTLparameterSynthesis.xml index 879113e..49444ab 100644 --- a/config/eBCSgen_parameterSynthesis.xml +++ b/config/eBCSgen_PCTLparameterSynthesis.xml @@ -1,8 +1,8 @@ - + - PCTL parameter synthesis of given model - python3 /home/xtrojak/eBCSgen/Callables/ParameterSynthesis.py - --model '$model' + python3 /home/xtrojak/eBCSgen/Callables/PCTLParameterSynthesis.py + --transition_file '$transition_file' #if len($regions) > 0: --output '$output_regions' #else: @@ -10,10 +10,6 @@ #end if --formula '$formula' - #if $bound != "": - --bound '$bound' - #end if - #set parameters = ",".join([str($s.from) + "=" + str($s.param) + "=" + str($s.to) for $s in $regions]) #if $parameters: --region '$parameters' @@ -21,11 +17,10 @@ - + - diff --git a/config/tours/PCTL-Model-Checking.yaml b/config/tours/PCTL-Model-Checking.yaml index fb7b480..7893363 100644 --- a/config/tours/PCTL-Model-Checking.yaml +++ b/config/tours/PCTL-Model-Checking.yaml @@ -13,29 +13,25 @@ steps: - title: Step 2 - Select tool element: >- #left > div.unified-panel > div.unified-panel-body > div > div.toolMenu > - div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(3) > a > + div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(4) > a > span.description content: "Click on PCTL Model Checking tool." placement: bottom - - title: Step 3 - Model file - element: 'div[tour_id="model"]' + - title: Step 3 - Computed Transition system + element: 'div[tour_id="transition_file"]' content: - "Choose BCSL model file.
- This tool supports only .bcs files stored in your history." + "You can choose a precomputed Transition System file.
+ This tool supports only .bcs.ts files stored in your history." placement: auto - title: Step 4 - PCTL Formula element: 'div[tour_id="formula"]' content: "Enter PCTL formula." placement: auto - - title: Step 5 - Bound - element: 'div[tour_id="bound"]' - content: "Specify agents boundary cap (optional)." - placement: auto - - title: Step 6 - Execute + - title: Step 5 - Execute element: '#execute' content: "Click the button Execute
to start model checking." placement: auto - - title: Step 7 - Results + - title: Step 6 - Results element: .list-items content: "Wait until the model checking is finished
diff --git a/config/tours/PCTL-Parameter-Synthesis.yaml b/config/tours/PCTL-Parameter-Synthesis.yaml index 82e10d8..5bbdf97 100644 --- a/config/tours/PCTL-Parameter-Synthesis.yaml +++ b/config/tours/PCTL-Parameter-Synthesis.yaml @@ -13,51 +13,46 @@ steps: - title: Step 2 - Select tool element: >- #left > div.unified-panel > div.unified-panel-body > div > div.toolMenu > - div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(4) > a + div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(5) > a content: "Click on PCTL Parameter Synthesis tool." placement: bottom - - title: Step 3 - Model file - element: 'div[tour_id="model"]' + - title: Step 3 - Computed Transition system + element: 'div[tour_id="transition_file"]' content: - "Choose BCSL model file.
- This tool supports only .bcs files stored in your history." - placement: auto + "You can choose a precomputed Transition System file.
+ This tool supports only .bcs.ts files stored in your history." - title: Step 4 - PCTL Formula element: 'div[tour_id="formula"]' content: "Enter PCTL formula." placement: auto - - title: Step 5 - Bound - element: 'div[tour_id="bound"]' - content: "Specify agents boundary cap (optional)." - placement: auto - - title: Step 6 - Insert Interval + - title: Step 5 - Insert Interval element: '#center .center-container .center-panel .ui-portlet .portlet-content .portlet-body .ui-form-element .ui-form-field button .ui-button-default.btn.btn-secondary.float-none.form-repeat-add' content: "Please specify values interval for
each unknown parameter." placement: auto - - title: Step 7 - Parameter name + - title: Step 6 - Parameter name element: 'div[tour_id="regions_0|param"]' content: "Enter parameter name." placement: bottom - - title: Step 8 - Parameter interval start + - title: Step 7 - Parameter interval start element: 'div[tour_id="regions_0|from"]' content: "Enter start of the interval." placement: bottom - - title: Step 9 - Parameter interval end + - title: Step 8 - Parameter interval end element: 'div[tour_id="regions_0|to"]' content: "Enter end of the interval." placement: bottom - - title: Step 10 - Delete Interval + - title: Step 9 - Delete Interval element: '#button_delete' content: "Option to delete your interval." placement: left - - title: Step 11 - Execute + - title: Step 10 - Execute element: '#execute' content: "Click the button Execute
to start parameter synthesis." placement: auto - - title: Step 12 - Results + - title: Step 11 - Results element: .list-items content: "Wait until the parameter synthesis is
diff --git a/config/tours/Probability-Sampling.yaml b/config/tours/Probability-Sampling.yaml index 747e019..371b8b3 100644 --- a/config/tours/Probability-Sampling.yaml +++ b/config/tours/Probability-Sampling.yaml @@ -13,7 +13,7 @@ steps: - title: Step 2 - Select tool element: >- #left > div.unified-panel > div.unified-panel-body > div > div.toolMenu > - div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(6) > a + div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(7) > a content: "Click on Probability Sampling tool." placement: bottom - title: Step 3 - Storm output file diff --git a/config/tours/SA-Context-Based-Reduction.yaml b/config/tours/SA-Context-Based-Reduction.yaml index eb60134..9ca37e8 100644 --- a/config/tours/SA-Context-Based-Reduction.yaml +++ b/config/tours/SA-Context-Based-Reduction.yaml @@ -15,7 +15,7 @@ steps: - title: Step 2 - Select tool element: >- #left > div.unified-panel > div.unified-panel-body > div > div.toolMenu > - div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(5) > a + div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(6) > a content: "Click on Static Analysis tool." placement: bottom - title: Step 3 - Model file diff --git a/config/tours/SA-non-reachibility.yaml b/config/tours/SA-non-reachibility.yaml index 46583f4..c3cd427 100644 --- a/config/tours/SA-non-reachibility.yaml +++ b/config/tours/SA-non-reachibility.yaml @@ -15,7 +15,7 @@ steps: - title: Step 2 - Select tool element: >- #left > div.unified-panel > div.unified-panel-body > div > div.toolMenu > - div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(5) > a + div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(6) > a content: "Click on Static Analysis tool." placement: bottom - title: Step 3 - Model file diff --git a/config/tours/SA-redundandancy-Elimination.yaml b/config/tours/SA-redundandancy-Elimination.yaml index 37f47f0..fe9666e 100644 --- a/config/tours/SA-redundandancy-Elimination.yaml +++ b/config/tours/SA-redundandancy-Elimination.yaml @@ -15,7 +15,7 @@ steps: - title: Step 2 - Select tool element: >- #left > div.unified-panel > div.unified-panel-body > div > div.toolMenu > - div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(5) > a + div:nth-child(4) > div > div > div:nth-child(2) > div:nth-child(6) > a content: "Click on Static Analysis tool." placement: bottom - title: Step 3 - Model file