edu.wis.jtlv.old_lib.mc
Class LTLModelChecker

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

public class LTLModelChecker
extends ModelChecker

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

The main interesting routines for EXTERNAL usage are:
valid(Spec) - Check validity of tl formula.
modelCheck(Spec) - Model check using a temporal formula.
modelCheckSeq(Spec) - Model check sequential program ( halted executions are extended indefinitely by adding the idle transition )
modelCheckTester(SMVModule) - Model check using a tester which is provided by the user in the

Version:

"1.3.2"

Author:

yaniv sa'ar.

Nested Class Summary

static class

LTLModelChecker.LTLTesterBuilder

Constructor Summary

LTLModelChecker(SMVModule design)

LTLModelChecker(SMVModule design, boolean removeRunningVar)

Method Summary

void	modelCheck(Spec property) Given a specification \phi (as a formula in temporal logic) we want to decide whether \phi is valid over finite state program P , i.e.
void	modelCheckStandardOutput(Spec property) Given a specification \phi (as a formula in temporal logic) we want to decide whether \phi is valid over finite state program P , i.e.
void	modelCheckTester(SMVModule user_tester) To compose a tester with the design, and perform model checking.
void	modelCheckTesterStandardOutput(SMVModule user_tester) To compose a tester with the design, and perform model checking.
boolean	modelCheckWithNoCounterExample(Spec property)
static void	standAloneValid(Spec property) Check validity for a given LTL property without any design attached.
static void	standAloneValidStarndardOutput(Spec property) Check validity for a given LTL property without any design attached.
void	valid(Spec property) Check validity for a given LTL property.
void	validStarndardOutput(Spec property) Check validity for a given LTL property.

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

LTLModelChecker

public LTLModelChecker(SMVModule design)
                throws ModelCheckException

Throws:

ModelCheckException

LTLModelChecker

public LTLModelChecker(SMVModule design,
                       boolean removeRunningVar)
                throws ModelCheckException

Throws:

ModelCheckException

Method Detail

modelCheckStandardOutput

public void modelCheckStandardOutput(Spec property)

Given a specification \phi (as a formula in temporal logic) we want to decide whether \phi is valid over finite state program P , i.e. whether all the computations of the design satisfy \phi. This variant of implementation, prints the results to the standard streams.

Parameters:

property - The property to check.

See Also:

modelCheck(Spec)

modelCheck

public void modelCheck(Spec property)
                throws ModelCheckException,
                       CounterExampleException

Given a specification \phi (as a formula in temporal logic) we want to decide whether \phi is valid over finite state program P , i.e. whether all the computations of the design satisfy \phi.

Parameters:

property - The property to check.

Throws:

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

CounterExampleException - When the property is not valid, a counter example is thrown.

See Also:

modelCheckStandardOutput(Spec)

modelCheckWithNoCounterExample

public boolean modelCheckWithNoCounterExample(Spec property)

modelCheckTesterStandardOutput

public void modelCheckTesterStandardOutput(SMVModule user_tester)

To compose a tester with the design, and perform model checking. If the composition is feasible then a counter example is thrown. This variant of implementation, prints the results to the standard streams.

Parameters:

user_tester - The tester to compose.

See Also:

modelCheckTester(SMVModule)

modelCheckTester

public void modelCheckTester(SMVModule user_tester)
                      throws CounterExampleException

To compose a tester with the design, and perform model checking. If the composition is feasible then a counter example is thrown.

Parameters:

user_tester - The tester to compose.

Throws:

CounterExampleException - When the property is not valid, a counter example is thrown.

See Also:

modelCheckTesterStandardOutput(SMVModule)

validStarndardOutput

public void validStarndardOutput(Spec property)

Check validity for a given LTL property. This variant of implementation, prints the results to the standard streams.

Parameters:

property - The property to check validity for.

See Also:

valid(Spec), standAloneValid(Spec), standAloneValidStarndardOutput(Spec)

valid

public void valid(Spec property)
           throws ModelCheckException

Check validity for a given LTL property.

Parameters:

property - The property to check validity for.

Throws:

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

CounterExampleException - When the property is not valid, a counter example is thrown.

See Also:

validStarndardOutput(Spec), standAloneValid(Spec), standAloneValidStarndardOutput(Spec)

standAloneValidStarndardOutput

public static void standAloneValidStarndardOutput(Spec property)

Check validity for a given LTL property without any design attached. This variant of implementation, prints the results to the standard streams.

Parameters:

property - The property to check validity for.

See Also:

valid(Spec), validStarndardOutput(Spec), standAloneValid(Spec)

standAloneValid

public static void standAloneValid(Spec property)
                            throws ModelCheckException

Check validity for a given LTL property without any design attached.

Parameters:

property - The property to check validity for.

Throws:

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

CounterExampleException - When the property is not valid, a counter example is thrown.

See Also:

valid(Spec), validStarndardOutput(Spec), standAloneValidStarndardOutput(Spec)