Let G be an activity graph. That is, each edge in G is labeled with an activity

Question

Let G be an activity graph. That is, each edge in G is labeled with an activity drawn from a finite set A. Each node in G is also called a state. Let s0 be a given initial state. In the definition of G, each node is either marked with good or not-good. Recall that a liveness property is to argue that something good will eventually happen. That is, it is not true that, from s0, there is an infinite path on G on which every state is marked with not-good. Design an algorithm to decide whether G satisfies the liveness property or not.

Explanation / Answer

Depth-first search determines that an accepting state has been reached, and all successors of that state have also been explored, it starts a nested search to see if the state is reachable from itself.
  
Store a copy of the accepting state in a global, called seed.

Store pairs of a state and a boolean variable toggle for stack and state space elements.

Stack D = {} ;   
Statespace V = {} ;
State seed = nil ;
Boolean toggle = false ;
Start() {
       Add_Statespace(V, A.s0, toggle) ;
       Push_Stack(D, A.s0, toggle) ;
Search() ;
}
Search() {
       (s, toggle) = Top_Stack(D) ;
       foreach (s, l, s

Related Questions

Navigate

• Browse (All)
• Browse L
• Subjects

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.