Module dev.civl.gmc

Package dev.civl.gmc.smc

Class SMC

java.lang.Object

dev.civl.gmc.smc.SMC

public class SMC
extends Object

This is a simple sequential model checker (SMC) implementing general model checker (GMC).
The main purposes is for both testing interfaces of GMC and providing and simple sequential implementation example for GMC.

Constructor Summary

Constructors

Constructor	Description
SMC()

Method Summary

Modifier and Type	Method	Description
boolean	run(MatrixDirectedGraph graph, StatePredicateIF<Integer> predicate, GMCConfiguration config)	For a given MatrixDirectedGraph graph and a predicate implementing StatePredicateIF, If the predicate is hold, true will be returned, else false. Note that the default starting state is the state with id of 0
boolean	run(MatrixDirectedGraph graph, StatePredicateIF<Integer> predicate, Integer initialState, GMCConfiguration config)	For a given MatrixDirectedGraph graph, a predicate implementing StatePredicateIF and a starting state initialState, If the predicate is hold, true will be returned, else false.
void	setDebug(boolean isDebug)	Set SMC to print debugging info, iff isDebug is true

Methods inherited from class java.lang.Object

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

Constructor Details

SMC

public SMC()

Method Details

run

public boolean run(MatrixDirectedGraph graph,
 StatePredicateIF<Integer> predicate,
 Integer initialState,
 GMCConfiguration config)

For a given MatrixDirectedGraph graph, a predicate implementing StatePredicateIF and a starting state initialState,
If the predicate is hold, true will be returned, else false.

Parameters:

graph - A MatrixDirectedGraph representing the transition map.

predicate - A predicate of a property

initialState - The starting state

Returns:

true iff there is a state in the violation state list, else false.

run

public boolean run(MatrixDirectedGraph graph,
 StatePredicateIF<Integer> predicate,
 GMCConfiguration config)

For a given MatrixDirectedGraph graph and a predicate implementing StatePredicateIF,
If the predicate is hold, true will be returned, else false.
Note that the default starting state is the state with id of 0

Parameters:

graph - A MatrixDirectedGraph representing the transition map.

predicate - A predicate of a property

Returns:

true iff there is a state in the violation state list, else false.

setDebug

public void setDebug(boolean isDebug)

Set SMC to print debugging info, iff isDebug is true