add explicit post to all eq. oracles

DES-Lab · May 11, 2021 · 91593a2 · 91593a2
1 parent 4d09f63
commit 91593a2
Show file tree

Hide file tree

Showing 9 changed files with 12 additions and 1 deletion.
diff --git a/aalpy/oracles/BreadthFirstExplorationEqOracle.py b/aalpy/oracles/BreadthFirstExplorationEqOracle.py
@@ -46,6 +46,7 @@ def find_cex(self, hypothesis):
                     self.num_steps += 1
 
                     if out_hyp != out_sul:
+                        self.sul.post()
                         return seq[:ind + 1]
 
         return None
diff --git a/aalpy/oracles/CacheBasedEqOracle.py b/aalpy/oracles/CacheBasedEqOracle.py
@@ -67,7 +67,7 @@ def find_cex(self, hypothesis):
                 if out_sul != out_hyp:
                     if self.reset_after_cex:
                         self.num_walks_done = 0
-
+                    self.sul.post()
                     return inputs
 
         return None

diff --git a/aalpy/oracles/RandomWalkEqOracle.py b/aalpy/oracles/RandomWalkEqOracle.py
@@ -53,6 +53,7 @@ def find_cex(self, hypothesis: Automaton):
                 if self.reset_after_cex:
                     self.random_steps_done = 0
 
+                self.sul.post()
                 return inputs
 
         return None
@@ -114,12 +115,14 @@ def find_cex(self, hypothesis):
                     self.random_steps_done = 0
 
                 if isinstance(hypothesis, Onfsm):
+                    self.sul.post()
                     return inputs, outputs
                 else:
                     # hypothesis is MDP or SMM
                     cex = [hypothesis.initial_state.output] if isinstance(hypothesis, Mdp) else []
                     for i, o in zip(inputs, outputs):
                         cex.extend([i, o])
+                    self.sul.post()
                     return cex
 
         return None
diff --git a/aalpy/oracles/RandomWordEqOracle.py b/aalpy/oracles/RandomWordEqOracle.py
@@ -53,6 +53,7 @@ def find_cex(self, hypothesis):
                     if self.reset_after_cex:
                         self.num_walks_done = 0
 
+                    self.sul.post()
                     return inputs
 
         return None

diff --git a/aalpy/oracles/StatePrefixEqOracle.py b/aalpy/oracles/StatePrefixEqOracle.py
@@ -70,6 +70,7 @@ def find_cex(self, hypothesis):
                 self.num_steps += 1
 
                 if out_sul != out_hyp:
+                    self.sul.post()
                     return prefix + suffix
 
         return None
diff --git a/aalpy/oracles/TransitionFocusOracle.py b/aalpy/oracles/TransitionFocusOracle.py
@@ -47,6 +47,7 @@ def find_cex(self, hypothesis):
                 self.num_steps += 1
 
                 if out_sul != out_hyp:
+                    self.sul.post()
                     return inputs
 
         return None
diff --git a/aalpy/oracles/UserInputEqOracle.py b/aalpy/oracles/UserInputEqOracle.py
@@ -47,6 +47,7 @@ def find_cex(self, hypothesis):
                 continue
             if inp == 'cex':
                 if inputs:
+                    self.sul.post()
                     return inputs
             if inp == 'end':
                 return None

diff --git a/aalpy/oracles/WMethodEqOracle.py b/aalpy/oracles/WMethodEqOracle.py
@@ -57,6 +57,7 @@ def find_cex(self, hypothesis):
 
                 outputs.append(out_sul)
                 if out_hyp != out_sul:
+                    self.sul.post()
                     return seq[:ind + 1]
             self.cache.add(seq)
 
@@ -114,6 +115,7 @@ def find_cex(self, hypothesis):
                 self.num_steps += 1
 
                 if output_sul != output_hyp:
+                    self.sul.post()
                     return test_case[:ind + 1]
 
         return None
diff --git a/aalpy/oracles/kWayStateCoverageEqOracle.py b/aalpy/oracles/kWayStateCoverageEqOracle.py
@@ -74,6 +74,7 @@ def find_cex(self, hypothesis):
                 self.num_steps += 1
 
                 if out_sul != out_hyp:
+                    self.sul.post()
                     return path[:i + 1]
 
         return None