Module dev.civl.gmc

Package dev.civl.gmc.concurrent

Class ConcurrentDfsSearcher<STATE,TRANSITION>

java.lang.Object

dev.civl.gmc.concurrent.ConcurrentDfsSearcher<STATE,TRANSITION>

Type Parameters:

STATE -

TRANSITION -

public class ConcurrentDfsSearcher<STATE,TRANSITION>
extends Object

This ConcurrentDfsSearcher is implemented based on Alfons Laarman's algorithm in paper "Partial-Order Reduction for Multi-Core LTL Model Checking", but there are improvements being made. Rather than a totally concurrent depth-first search, it may be more appropriate to say that the algorithm consists of multiple sequential depth-first search that are synchronized to some extent.

The basic idea is using multiple threads to search through the state space, each of them starts a depth-first search with its own stack. And try to make them search different parts of the state space.

Constructor Summary

Constructors

Constructor	Description
ConcurrentDfsSearcher(EnablerIF<STATE,TRANSITION> enabler, ConcurrentStateManagerIF<STATE,TRANSITION> manager, StatePredicateIF<STATE> predicate, int N)

Method Summary

Modifier and Type	Method	Description
boolean	cycleFound()
boolean	getMinimize()
String	name()
StatePredicateIF<STATE>	predicate()
boolean	reportCycleAsViolation()
boolean	search(STATE initialState)	Start a concurrent dfs task from a given state
void	setMinimize(boolean value)
void	setName(String name)
void	setReportCycleAsViolation(boolean value)	If you want to check for cycles in the state space, and report the existence of a cycle as a violation, this flag should be set to true.
int	totalNumStatesMatched()	The number of states matched so far.
int	totalNumStatesSeen()	The number of states seen in this search.
int	totalNumTransitions()	The number of transitions executed in the course of this search so far.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

ConcurrentDfsSearcher

public ConcurrentDfsSearcher(EnablerIF<STATE,TRANSITION> enabler,
 ConcurrentStateManagerIF<STATE,TRANSITION> manager,
 StatePredicateIF<STATE> predicate,
 int N)

Method Details

predicate

public StatePredicateIF<STATE> predicate()

setName

public void setName(String name)

name

public String name()

setMinimize

public void setMinimize(boolean value)

getMinimize

public boolean getMinimize()

reportCycleAsViolation

public boolean reportCycleAsViolation()

setReportCycleAsViolation

public void setReportCycleAsViolation(boolean value)

If you want to check for cycles in the state space, and report the existence of a cycle as a violation, this flag should be set to true. Else set it to false. By default, it is false.

cycleFound

public boolean cycleFound()

totalNumStatesSeen

public int totalNumStatesSeen()

The number of states seen in this search.

Returns:

the number of states seen so far

totalNumTransitions

public int totalNumTransitions()

The number of transitions executed in the course of this search so far.

Returns:

the number of transitions executed.

totalNumStatesMatched

public int totalNumStatesMatched()

The number of states matched so far. A state is "matched" when the search determines the state has been seen before, earlier in the search. If the state has been seen before, it is not explored.

Returns:

the number of states matched

search

public boolean search(STATE initialState)

Start a concurrent dfs task from a given state

Parameters:

initialState - The state the search starts from.

Throws:

Exception