From 92a0f1fe70ab78bd84cf4f6ffd0d60f7c2a38456 Mon Sep 17 00:00:00 2001 From: tomyaacov Date: Sun, 27 Aug 2023 18:41:19 +0300 Subject: [PATCH 1/9] adding swig to tools --- .readthedocs.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index 197df79..db98846 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -9,6 +9,7 @@ build: os: ubuntu-22.04 tools: python: "3.7" + swig: "latest" python: install: From 77949e24ad9dc0106acf5d25e21c0211de3dcbc8 Mon Sep 17 00:00:00 2001 From: tomyaacov Date: Sun, 27 Aug 2023 18:43:45 +0300 Subject: [PATCH 2/9] adding swig to tools --- .readthedocs.yaml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index db98846..d865340 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -8,8 +8,7 @@ version: 2 build: os: ubuntu-22.04 tools: - python: "3.7" - swig: "latest" + python: "3.9" python: install: From 1d342f218776d8912f737177fc71f2558322912d Mon Sep 17 00:00:00 2001 From: tomyaacov Date: Sun, 27 Aug 2023 18:58:09 +0300 Subject: [PATCH 3/9] updating docs and examples with analysis module --- docs/requirements.txt | 1 - 1 file changed, 1 deletion(-) diff --git a/docs/requirements.txt b/docs/requirements.txt index b1ae199..3ba814c 100644 --- a/docs/requirements.txt +++ b/docs/requirements.txt @@ -2,6 +2,5 @@ git+https://github.com/bThink-BGU/BPpy.git@master z3-solver>=4.8.5.0 gymnasium==0.28.1 stable-baselines3==2.0.0 -pynusmv==1.0rc8 From b88ff51318949f1ad17a824f7d4b3beb4acf0a73 Mon Sep 17 00:00:00 2001 From: tomyaacov Date: Mon, 28 Aug 2023 09:03:38 +0300 Subject: [PATCH 4/9] updating pynusmv import level --- bppy/analysis/symbolic_bprogram_verifier.py | 34 +++++++++++++-------- 1 file changed, 21 insertions(+), 13 deletions(-) diff --git a/bppy/analysis/symbolic_bprogram_verifier.py b/bppy/analysis/symbolic_bprogram_verifier.py index f9875a8..b3508a8 100644 --- a/bppy/analysis/symbolic_bprogram_verifier.py +++ b/bppy/analysis/symbolic_bprogram_verifier.py @@ -4,18 +4,7 @@ from bppy.model.event_selection.simple_event_selection_strategy import SimpleEventSelectionStrategy import sys import tempfile -try: - import pynusmv - from pynusmv.model import * - from pynusmv.mc import check_ltl_spec, check_explain_ltl_spec - from pynusmv.bmc.glob import bmc_setup, BmcSupport, master_be_fsm - from pynusmv.parser import parse_ltl_spec - from pynusmv.node import Node - from pynusmv.sat import SatSolverFactory, Polarity, SatSolverResult - from pynusmv.bmc import ltlspec, utils as bmcutils -except ImportError: - raise ImportError("PyNuSMV is not installed. Please install it to use SymbolicBProgramVerifier. More info on " - "PyNuSMV installation can be found at https://github.com/LouvainVerificationLab/pynusmv") + class SymbolicBProgramVerifier: @@ -44,6 +33,7 @@ def __init__(self, bprogram_generator, event_list): self.bprogram_generator = bprogram_generator self.event_list = event_list self.bthread_num = len(self.bprogram_generator().bthreads) + self._import_package() sys.setrecursionlimit(10000) def verify(self, spec, type="BDD", bound=1000, find_counterexample=False, print_info=False): @@ -72,6 +62,13 @@ def verify(self, spec, type="BDD", bound=1000, find_counterexample=False, print_ Optional[str]: A counterexample, if one exists and find_counterexample is True. Otherwise, None. """ + import pynusmv + from pynusmv.mc import check_ltl_spec, check_explain_ltl_spec + from pynusmv.bmc.glob import bmc_setup, BmcSupport, master_be_fsm + from pynusmv.parser import parse_ltl_spec + from pynusmv.node import Node + from pynusmv.sat import SatSolverFactory, Polarity, SatSolverResult + from pynusmv.bmc import ltlspec, utils as bmcutils if print_info: print("initializing NuSMV") pynusmv.init.init_nusmv() @@ -175,6 +172,7 @@ def verify(self, spec, type="BDD", bound=1000, find_counterexample=False, print_ return result, explanation_str def _bthread_to_module(self, bthread_generator, bthread_name, event_list): + from pynusmv.model import Identifier, Var, Range, Boolean, Trueexp, Falseexp, Case, And, Or, Module dfs = DFSBThread(bthread_generator, SimpleEventSelectionStrategy(), event_list) init_s, visited, requested, blocked = dfs.run(return_requested_and_blocked=True) @@ -259,6 +257,8 @@ def _bthread_to_module(self, bthread_generator, bthread_name, event_list): return type(bthread_name, (Module,), bt1_mod_dict) def _main_module(self, event_list, bt_list): + import pynusmv + from pynusmv.model import Var, Trueexp, Falseexp, Case, And, Or, Module, Scalar, Implies, NotEqual, Equal mod_dict = {} mod_dict["event"] = Var(Scalar(tuple(["BPROGRAM_START", "BPROGRAM_DONE"] + [x.name for x in event_list]))) bt_modules = [] @@ -294,4 +294,12 @@ def _main_module(self, event_list, bt_list): trans_statement = And(trans_statement, Implies(any_enabled, NotEqual("next(event)", "BPROGRAM_DONE"))) trans_statement = And(trans_statement, Implies(Equal("event", "BPROGRAM_DONE"), Equal("next(event)", "BPROGRAM_DONE"))) mod_dict["TRANS"] = [trans_statement] - return type("main", (Module,), mod_dict) \ No newline at end of file + return type("main", (Module,), mod_dict) + + def _import_package(self): + try: + import pynusmv + except ImportError: + print("PyNuSMV is not installed. Please install it to use SymbolicBProgramVerifier. More info on ") + print("PyNuSMV installation can be found at https://github.com/LouvainVerificationLab/pynusmv") + sys.exit(0) From 7650af05ca262b40006987face7af4e1e6e59de2 Mon Sep 17 00:00:00 2001 From: tomyaacov Date: Mon, 28 Aug 2023 09:22:09 +0300 Subject: [PATCH 5/9] updating pynusmv import level --- bppy/analysis/symbolic_bprogram_verifier.py | 32 ++++++++------------- 1 file changed, 12 insertions(+), 20 deletions(-) diff --git a/bppy/analysis/symbolic_bprogram_verifier.py b/bppy/analysis/symbolic_bprogram_verifier.py index b3508a8..5aaaf7c 100644 --- a/bppy/analysis/symbolic_bprogram_verifier.py +++ b/bppy/analysis/symbolic_bprogram_verifier.py @@ -4,7 +4,18 @@ from bppy.model.event_selection.simple_event_selection_strategy import SimpleEventSelectionStrategy import sys import tempfile - +try: + import pynusmv + from pynusmv.model import * + from pynusmv.mc import check_ltl_spec, check_explain_ltl_spec + from pynusmv.bmc.glob import bmc_setup, BmcSupport, master_be_fsm + from pynusmv.parser import parse_ltl_spec + from pynusmv.node import Node + from pynusmv.sat import SatSolverFactory, Polarity, SatSolverResult + from pynusmv.bmc import ltlspec, utils as bmcutils +except ImportError: + raise ImportError("PyNuSMV is not installed. Please install it to use SymbolicBProgramVerifier. More info on " + "PyNuSMV installation can be found at https://github.com/LouvainVerificationLab/pynusmv") class SymbolicBProgramVerifier: @@ -33,7 +44,6 @@ def __init__(self, bprogram_generator, event_list): self.bprogram_generator = bprogram_generator self.event_list = event_list self.bthread_num = len(self.bprogram_generator().bthreads) - self._import_package() sys.setrecursionlimit(10000) def verify(self, spec, type="BDD", bound=1000, find_counterexample=False, print_info=False): @@ -62,13 +72,6 @@ def verify(self, spec, type="BDD", bound=1000, find_counterexample=False, print_ Optional[str]: A counterexample, if one exists and find_counterexample is True. Otherwise, None. """ - import pynusmv - from pynusmv.mc import check_ltl_spec, check_explain_ltl_spec - from pynusmv.bmc.glob import bmc_setup, BmcSupport, master_be_fsm - from pynusmv.parser import parse_ltl_spec - from pynusmv.node import Node - from pynusmv.sat import SatSolverFactory, Polarity, SatSolverResult - from pynusmv.bmc import ltlspec, utils as bmcutils if print_info: print("initializing NuSMV") pynusmv.init.init_nusmv() @@ -172,7 +175,6 @@ def verify(self, spec, type="BDD", bound=1000, find_counterexample=False, print_ return result, explanation_str def _bthread_to_module(self, bthread_generator, bthread_name, event_list): - from pynusmv.model import Identifier, Var, Range, Boolean, Trueexp, Falseexp, Case, And, Or, Module dfs = DFSBThread(bthread_generator, SimpleEventSelectionStrategy(), event_list) init_s, visited, requested, blocked = dfs.run(return_requested_and_blocked=True) @@ -257,8 +259,6 @@ def _bthread_to_module(self, bthread_generator, bthread_name, event_list): return type(bthread_name, (Module,), bt1_mod_dict) def _main_module(self, event_list, bt_list): - import pynusmv - from pynusmv.model import Var, Trueexp, Falseexp, Case, And, Or, Module, Scalar, Implies, NotEqual, Equal mod_dict = {} mod_dict["event"] = Var(Scalar(tuple(["BPROGRAM_START", "BPROGRAM_DONE"] + [x.name for x in event_list]))) bt_modules = [] @@ -295,11 +295,3 @@ def _main_module(self, event_list, bt_list): trans_statement = And(trans_statement, Implies(Equal("event", "BPROGRAM_DONE"), Equal("next(event)", "BPROGRAM_DONE"))) mod_dict["TRANS"] = [trans_statement] return type("main", (Module,), mod_dict) - - def _import_package(self): - try: - import pynusmv - except ImportError: - print("PyNuSMV is not installed. Please install it to use SymbolicBProgramVerifier. More info on ") - print("PyNuSMV installation can be found at https://github.com/LouvainVerificationLab/pynusmv") - sys.exit(0) From f52336dfd03181c2d3bdb0456f9aba0c622670f5 Mon Sep 17 00:00:00 2001 From: tomyaacov Date: Mon, 28 Aug 2023 09:22:34 +0300 Subject: [PATCH 6/9] adding swig --- .readthedocs.yaml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index d865340..e9ec33c 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -9,6 +9,8 @@ build: os: ubuntu-22.04 tools: python: "3.9" + apt_packages: + - swig python: install: From 3a46376367d36886d500b0c199f58e7be6c56468 Mon Sep 17 00:00:00 2001 From: tomyaacov Date: Mon, 28 Aug 2023 09:27:59 +0300 Subject: [PATCH 7/9] adding pynusmv to docs requirements --- docs/requirements.txt | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/docs/requirements.txt b/docs/requirements.txt index 3ba814c..01da427 100644 --- a/docs/requirements.txt +++ b/docs/requirements.txt @@ -2,5 +2,4 @@ git+https://github.com/bThink-BGU/BPpy.git@master z3-solver>=4.8.5.0 gymnasium==0.28.1 stable-baselines3==2.0.0 - - +pynusmv==1.0rc8 From 6c97d6121af5a172376af05b5094e83a7ec5e05e Mon Sep 17 00:00:00 2001 From: tomyaacov Date: Mon, 28 Aug 2023 09:33:16 +0300 Subject: [PATCH 8/9] adding flex bison patchelf --- .readthedocs.yaml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.readthedocs.yaml b/.readthedocs.yaml index e9ec33c..1ad8844 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -11,6 +11,9 @@ build: python: "3.9" apt_packages: - swig + - flex + - bison + - patchelf python: install: From 266c8212a87f712b488ef5d051714deef52958ca Mon Sep 17 00:00:00 2001 From: tomyaacov Date: Mon, 28 Aug 2023 09:41:31 +0300 Subject: [PATCH 9/9] adding pynusmv to docs requirements --- docs/requirements.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/requirements.txt b/docs/requirements.txt index 01da427..a692c1a 100644 --- a/docs/requirements.txt +++ b/docs/requirements.txt @@ -2,4 +2,4 @@ git+https://github.com/bThink-BGU/BPpy.git@master z3-solver>=4.8.5.0 gymnasium==0.28.1 stable-baselines3==2.0.0 -pynusmv==1.0rc8 +https://github.com/davidebreso/pynusmv/releases/download/v1.0rc8/pynusmv-1.0rc8-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl