← Back to branch summary

~yrke/opaal/timedart-vars+discrete

« back to all changes in this revision

Viewing changes to opaal/modelchecking_algorithms/reachability.py

  • Committer: Kenneth Yrke Jørgensen
  • Date: 2011-05-17 08:07:38 UTC
  • mfrom: (37.1.19 timedart-vars)
  • Revision ID: mail@yrke.dk-20110517080738-y09sdczr3npky2af
Merged with vars

Show diffs side-by-side

added added

removed removed

Lines of Context:
opaal/modelchecking_algorithms/reachability.py
16
16
 
17
17
from opaal.passed_waiting_list import NoMoreStatesException, GoalFoundException
18
18
 
 
19
import logging
 
20
logger = logging.getLogger('reachability')
 
21
 
 
22
 
19
23
class McReachability:
20
24
    def __init__(self, succgen, goalchecker, pwlist):
21
25
        self.succgen = succgen
27
31
    def __1step(self):
28
32
        """Computes a single step."""
29
33
        state = self.pwlist.getWaitingState()
 
34
        w,p = self.pwlist.getWP(state)
 
35
        self.pwlist.setWP(state, w,w) #Mark state as explored
 
36
       
 
37
        if (p == w): #Already checked
 
38
            #logger.debug("Already checked state on pw list %s - %s - %s", state, w, p)
 
39
            return
 
40
 
30
41
        if self.goalchecker.isGoal(state):
31
42
            raise GoalFoundException
32
 
        for succ in self.succgen.successors(state):
33
 
            self.pwlist.addState(succ)
 
43
        for succ, w, p in self.succgen.successors(state, w, p):
 
44
            self.pwlist.addState(succ, w, p)
34
45
            self.processed_states += 1
35
46
 
36
47
    def compute(self, steps=1):