edu.wis.jtlv.old_lib.mc
Class SimpleModelChecker

java.lang.Object
  edu.wis.jtlv.old_lib.mc.ModelChecker
      edu.wis.jtlv.old_lib.mc.SimpleModelChecker

public class SimpleModelChecker
extends ModelChecker

A wrapper to a SMVModule which knows how to check simple properties for the given module.

Version:

"1.3.2"

Author:

yaniv sa'ar.

Constructor Summary

SimpleModelChecker(SMVModule design)

SimpleModelChecker(SMVModule design, boolean removeRunningVar)

Method Summary

void	checkDeadlock() Deadlocked states are those whose only successor is them-self.
void	checkDeadlockStrandardOutput() Deadlocked states are those whose only successor is them-self.
void	checkInvariance(Spec property) The invariance procedure check that a property holds on all reachable states.
void	checkInvarianceStrandardOutput(Spec property) The invariance procedure check that a property holds on all reachable states.
void	checkReact(Spec p, Spec[] q, Spec r) Verify whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid.
void	checkReactStrandardOutput(Spec p, Spec[] q, Spec r) Verify whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid.
void	checkTempEntail(Spec p, Spec q) Verify whether [](p -> <>q) is valid.
void	checkTempEntailStrandardOutput(Spec p, Spec q) Verify whether [](p -> <>q) is valid.

Methods inherited from class edu.wis.jtlv.old_lib.mc.ModelChecker

getDesign

Methods inherited from class java.lang.Object

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

Constructor Detail

SimpleModelChecker

public SimpleModelChecker(SMVModule design)
                   throws ModelCheckException

Throws:

ModelCheckException

SimpleModelChecker

public SimpleModelChecker(SMVModule design,
                          boolean removeRunningVar)
                   throws ModelCheckException

Throws:

ModelCheckException

Method Detail

checkDeadlockStrandardOutput

public void checkDeadlockStrandardOutput()

Deadlocked states are those whose only successor is them-self. This method variant checks for the absence of deadlocks in the module in prints the results to the standard streams.

See Also:

checkDeadlock()

checkDeadlock

public void checkDeadlock()
                   throws CounterExampleException

Deadlocked states are those whose only successor is them-self. This method checks for the absence of deadlocks in the module.

Throws:

CounterExampleException - When the property does not hold on some reachable state, a counter example is thrown.

See Also:

checkDeadlockStrandardOutput()

checkInvarianceStrandardOutput

public void checkInvarianceStrandardOutput(Spec property)

The invariance procedure check that a property holds on all reachable states. This variant of implementation, prints the results to the standard streams.

Parameters:

property - The property to check invariance for.

See Also:

checkInvariance(Spec)

checkInvariance

public void checkInvariance(Spec property)
                     throws ModelCheckException,
                            CounterExampleException

The invariance procedure check that a property holds on all reachable states.

Parameters:

property - The property to check invariance for.

Throws:

ModelCheckException - When the invariance method is initiated with other then propositional property.

CounterExampleException - When the property does not hold on some reachable state, a counter example is thrown.

See Also:

checkInvarianceStrandardOutput(Spec)

checkTempEntailStrandardOutput

public void checkTempEntailStrandardOutput(Spec p,
                                           Spec q)

Verify whether [](p -> <>q) is valid. This variant of implementation, prints the results to the standard streams.

Parameters:

p - The first propositional property.

q - The second propositional property.

See Also:

checkTempEntail(Spec, Spec)

checkTempEntail

public void checkTempEntail(Spec p,
                            Spec q)
                     throws ModelCheckException,
                            CounterExampleException

Verify whether [](p -> <>q) is valid.

Parameters:

p - The first propositional property.

q - The second propositional property.

Throws:

ModelCheckException - When the tempEntail method is initiated with other then propositional properties.

CounterExampleException - When the TempEntail fails, a counter example is thrown.

See Also:

checkTempEntailStrandardOutput(Spec, Spec)

checkReactStrandardOutput

public void checkReactStrandardOutput(Spec p,
                                      Spec[] q,
                                      Spec r)

Verify whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid. This variant of implementation, prints the results to the standard streams.

Parameters:

p - The first propositional property.

q - An array of always eventually properties

r - The second propositional property.

See Also:

checkReact(Spec, Spec[], Spec)

checkReact

public void checkReact(Spec p,
                       Spec[] q,
                       Spec r)
                throws ModelCheckException,
                       CounterExampleException

Verify whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid.

Parameters:

p - The first propositional property.

q - An array of always eventually properties

r - The second propositional property.

Throws:

ModelCheckException - When the checkReact method is initiated with other then propositional properties.

CounterExampleException - When the checkReact fails, a counter example is thrown.

See Also:

checkReactStrandardOutput(Spec, Spec[], Spec)