Retry restarting (thx again Bernard)

Author: nicolasAmat

smpt/checkers/bulk.py

@@ -43,7 +43,7 @@ class Bulk(AbstractChecker):
     Bulk meta method.
     """
 
-    def __init__(self, ptnet: PetriNet, formula: Formula, properties: Properties, formula_compound: Formula, pdr: bool = False, slice : bool = False, debug: bool = False, solver_pids: Optional[Queue[int]] = None, bulk_techniques: Optional[Queue[str]] = None):
+    def __init__(self, ptnet: PetriNet, formula: Formula, properties: Properties, formula_compound: Formula, pdr: bool = False, slice : bool = False, high_restart: bool = False, debug: bool = False, solver_pids: Optional[Queue[int]] = None, bulk_techniques: Optional[Queue[str]] = None):
         """ Initializer.
         """
         # Local queue of solver pids (for PDR)
@@ -55,7 +55,7 @@ def __init__(self, ptnet: PetriNet, formula: Formula, properties: Properties, fo
         # Methods
         self.pdr = PDR(ptnet, formula, debug=debug, method='REACH', saturation=True, solver_pids=solver_pids, solver_pids_bis=self.solver_pids_bis) if pdr else None
         self.compound = Compound(formula_compound, properties, debug=debug, solver_pids=solver_pids)
-        self.walk = RandomWalk(ptnet, formula, slice=slice, debug=debug, solver_pids=solver_pids)
+        self.walk = RandomWalk(ptnet, formula, slice=slice, high_restart=high_restart, debug=debug, solver_pids=solver_pids)
 
     def prove(self, result, concurrent_pids):
         """ Prover.

smpt/checkers/randomwalk.py

@@ -43,7 +43,7 @@ class RandomWalk(AbstractChecker):
     """ Random walk method.
     """
 
-    def __init__(self, ptnet: PetriNet, formula: Formula, parikh: bool = False, slice: bool = False, debug: bool = False, solver_pids: Optional[Queue[int]] = None, additional_techniques: Optional[Queue[str]] = None):
+    def __init__(self, ptnet: PetriNet, formula: Formula, parikh: bool = False, slice: bool = False, high_restart: bool = False, debug: bool = False, solver_pids: Optional[Queue[int]] = None, additional_techniques: Optional[Queue[str]] = None):
         """ Initializer.
         """
         # Initial Petri net and formula
@@ -56,11 +56,13 @@ def __init__(self, ptnet: PetriNet, formula: Formula, parikh: bool = False, slic
         # Slicing
         self.slice = not self.parikh and slice
 
+        max_markings = 100000 if high_restart else 1000000
+
         # Walkers
         if self.parikh:
-            self.solver = Walk(ptnet.filename, parikh_filename=formula.parikh_filename, debug=debug, solver_pids=solver_pids)
+            self.solver = Walk(ptnet.filename, parikh_filename=formula.parikh_filename, max_markings=max_markings, debug=debug, solver_pids=solver_pids)
         else:
-            self.solver = Walk(ptnet.filename, slice=self.slice, debug=debug, solver_pids=solver_pids)
+            self.solver = Walk(ptnet.filename, slice=self.slice, max_markings=max_markings, debug=debug, solver_pids=solver_pids)
 
         # Additional techniques queue
         self.additional_techniques = additional_techniques

smpt/exec/parallelizer.py

@@ -314,10 +314,10 @@ def prove(self, method: str, result, concurrent_pids: Queue[list[int]]) -> None:
         prover : Optional[AbstractChecker] = None
 
         if method == 'WALK':
-            prover = RandomWalk(self.ptnet_walk_pdr, self.formula_walk_pdr, parikh=True, slice=self.slice, debug=self.debug, solver_pids=self.solver_pids, additional_techniques=self.additional_techniques)
+            prover = RandomWalk(self.ptnet_walk_pdr, self.formula_walk_pdr, parikh=True, slice=self.slice, high_restart=self.pre_run, debug=self.debug, solver_pids=self.solver_pids, additional_techniques=self.additional_techniques)
 
         if method == 'WALK-NO-PARIKH':
-            prover = RandomWalk(self.ptnet_walk_pdr, self.formula_walk_pdr, parikh=False, slice=self.slice, debug=self.debug, solver_pids=self.solver_pids, additional_techniques=self.additional_techniques)
+            prover = RandomWalk(self.ptnet_walk_pdr, self.formula_walk_pdr, parikh=False, slice=self.slice,  high_restart=self.pre_run, debug=self.debug, solver_pids=self.solver_pids, additional_techniques=self.additional_techniques)
 
         elif method == 'STATE-EQUATION':
             prover = StateEquation(self.ptnet_state_equation, self.formula_state_equation, ptnet_reduced=self.ptnet_reduced_state_equation, system=self.system_state_equation, ptnet_skeleton=self.ptnet_skeleton, formula_skeleton=self.formula_skeleton, pre_run=self.pre_run, debug=self.debug, solver_pids=self.solver_pids, additional_techniques=self.additional_techniques)
@@ -353,10 +353,10 @@ def prove(self, method: str, result, concurrent_pids: Queue[list[int]]) -> None:
             prover = InitialMarking(self.ptnet_skeleton, self.formula)
 
         elif method == 'BULK-PDR-COMPOUND-WALK':
-            prover = Bulk(self.ptnet_walk_pdr, self.formula_walk_pdr, self.properties, self.formula, pdr=True, slice=self.slice, debug=self.debug, solver_pids=self.solver_pids, bulk_techniques=self.bulk_techniques)
+            prover = Bulk(self.ptnet_walk_pdr, self.formula_walk_pdr, self.properties, self.formula, pdr=True, slice=self.slice, high_restart=self.pre_run, debug=self.debug, solver_pids=self.solver_pids, bulk_techniques=self.bulk_techniques)
 
         elif method == 'BULK-COMPOUND-WALK':
-            prover = Bulk(self.ptnet_walk_pdr, self.formula_walk_pdr, self.properties, self.formula, pdr=False, slice=self.slice, debug=self.debug, solver_pids=self.solver_pids, bulk_techniques=self.bulk_techniques)
+            prover = Bulk(self.ptnet_walk_pdr, self.formula_walk_pdr, self.properties, self.formula, pdr=False, slice=self.slice, high_restart=self.pre_run, debug=self.debug, solver_pids=self.solver_pids, bulk_techniques=self.bulk_techniques)
 
         if prover:
             prover.prove(result, concurrent_pids)

smpt/interfaces/walk.py

@@ -53,6 +53,8 @@ class Walk(Solver):
         Path to an eventual Parikh file.
     solver : Popen, optional
         A walk process.
+    max_markings : int
+        Max markings to explore before restarting.
     timeout : int
         Timeout of walk.
     solver_pids : Queue of int
@@ -63,7 +65,7 @@ class Walk(Solver):
         Debugging flag.
     """
 
-    def __init__(self, ptnet_filename: str, slice: bool = False, parikh_filename: Optional[str] = None, debug: bool = False, timeout: int = 0, solver_pids: Optional[Queue[int]] = None) -> None:
+    def __init__(self, ptnet_filename: str, slice: bool = False, parikh_filename: Optional[str] = None, max_markings: int = 1000000, debug: bool = False, timeout: int = 0, solver_pids: Optional[Queue[int]] = None) -> None:
         """ Initializer.
 
         Parameters
@@ -74,6 +76,8 @@ def __init__(self, ptnet_filename: str, slice: bool = False, parikh_filename: Op
             Slicing mode.
         parikh_filename : str, optional
             Path to an eventual Parikh file.
+        max_markings : int, optional
+            Max markings to explore before restarting.
         debug: bool, optional
             Debugging flag.
         timeout: int, optional
@@ -92,6 +96,7 @@ def __init__(self, ptnet_filename: str, slice: bool = False, parikh_filename: Op
 
         # Solver
         self.solver: Optional[Popen] = None
+        self.max_markings: int = max_markings
         self.timeout: int = timeout
         self.solver_pids: Queue[int] = solver_pids
 
@@ -159,7 +164,7 @@ def check_sat(self, walk_filename: str = None) -> bool:
         if walk_filename is None:
             raise ValueError("Walk: no filename")
 
-        process = ['walk', '-R', '-loop', '-seed', self.ptnet_filename, '-ff', walk_filename]
+        process = ['walk', '-R', '-c', str(self.max_markings), '-loop', '-seed', self.ptnet_filename, '-ff', walk_filename]
 
         if self.parikh_filename:
             process += ['-favor', self.parikh_filename]