Package net.automatalib.modelchecker.ltsmin.ltl

Class LTSminLTLAlternating<I,O>

java.lang.Object

net.automatalib.modelchecker.ltsmin.AbstractLTSmin<I,A,L>

net.automatalib.modelchecker.ltsmin.ltl.AbstractLTSminLTL<I,MealyMachine<?,I,?,O>,Lasso.MealyLasso<I,O>>

net.automatalib.modelchecker.ltsmin.ltl.AbstractLTSminLTLMealy<I,O>

net.automatalib.modelchecker.ltsmin.ltl.LTSminLTLAlternating<I,O>

Type Parameters:

I - the input type

O - the output type

All Implemented Interfaces:

LTSmin<I,MealyMachine<?,I,?,O>,Lasso.MealyLasso<I,O>>, LTSminAlternating<I,O,Lasso.MealyLasso<I,O>>, LTSminMealy<I,O,Lasso.MealyLasso<I,O>>, ModelChecker<I,MealyMachine<?,I,?,O>,String,Lasso.MealyLasso<I,O>>, ModelChecker.MealyModelChecker<I,O,String,Lasso.MealyLasso<I,O>>, ModelCheckerLasso<I,MealyMachine<?,I,?,O>,String,Lasso.MealyLasso<I,O>>, ModelCheckerLasso.MealyModelCheckerLasso<I,O,String>

public class LTSminLTLAlternating<I,O>
extends AbstractLTSminLTLMealy<I,O>
implements LTSminAlternating<I,O,Lasso.MealyLasso<I,O>>

An LTL model checker using LTSmin for Mealy machines using alternating edge semantics.

Nested Class Summary

Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelChecker

ModelChecker.DFAModelChecker<I,P,R>, ModelChecker.MealyModelChecker<I,O,P,R>

Nested classes/interfaces inherited from interface net.automatalib.modelchecking.ModelCheckerLasso

ModelCheckerLasso.DFAModelCheckerLasso<I,P>, ModelCheckerLasso.MealyModelCheckerLasso<I,O,P>

Field Summary

Fields inherited from class net.automatalib.modelchecker.ltsmin.ltl.AbstractLTSminLTL

REQUIRED_VERSION

Constructor Summary

Constructors

Constructor	Description
LTSminLTLAlternating(boolean keepFiles, Function<String,I> string2Input, Function<String,O> string2Output, int minimumUnfolds, double multiplier, Collection<? super O> skipOutputs)

Method Summary

Modifier and Type	Method	Description
boolean	requiresOriginalAutomaton()	Whether this model checker requires the original Mealy machine to read the Mealy machines from an FSM.
protected void	verifyFormula(String formula)	This method must verify that the given formula adheres to the expected syntax of the chosen serialization format for hypotheses of this model-checker.

Methods inherited from class net.automatalib.modelchecker.ltsmin.ltl.AbstractLTSminLTLMealy

findCounterExample, getSkipOutputs, getString2Output, setSkipOutputs

Methods inherited from class net.automatalib.modelchecker.ltsmin.ltl.AbstractLTSminLTL

getExtraCommandLineOptions, getMinimumRequiredVersion, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier

Methods inherited from class net.automatalib.modelchecker.ltsmin.AbstractLTSmin

findCounterExampleFSM, getString2Input, isKeepFiles

Methods inherited from class java.lang.Object

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

Methods inherited from interface net.automatalib.modelchecker.ltsmin.LTSmin

getString2Input, isKeepFiles

Methods inherited from interface net.automatalib.modelchecker.ltsmin.LTSminAlternating

fsm2Mealy, mealy2ETF

Methods inherited from interface net.automatalib.modelchecker.ltsmin.LTSminMealy

automaton2ETF, getString2Output

Methods inherited from interface net.automatalib.modelchecking.ModelChecker

findCounterExample

Methods inherited from interface net.automatalib.modelchecking.ModelChecker.MealyModelChecker

getSkipOutputs, setSkipOutputs

Methods inherited from interface net.automatalib.modelchecking.ModelCheckerLasso

computeUnfolds, getMinimumUnfolds, getMultiplier, setMinimumUnfolds, setMultiplier

Constructor Detail

LTSminLTLAlternating

public LTSminLTLAlternating(boolean keepFiles,
                            Function<String,I> string2Input,
                            Function<String,O> string2Output,
                            int minimumUnfolds,
                            double multiplier,
                            Collection<? super O> skipOutputs)

Method Detail

requiresOriginalAutomaton

public boolean requiresOriginalAutomaton()

Description copied from interface: LTSminAlternating

Whether this model checker requires the original Mealy machine to read the Mealy machines from an FSM.

Specified by:

requiresOriginalAutomaton in interface LTSminAlternating<I,O,Lasso.MealyLasso<I,O>>

Returns:

false, because only lassos should be read from FSMs.

verifyFormula

protected void verifyFormula(String formula)

Description copied from class: AbstractLTSmin

This method must verify that the given formula adheres to the expected syntax of the chosen serialization format for hypotheses of this model-checker.

If the formula does not adhere to the expected syntax, this method should throw a IllegalArgumentException, possibly containing nested causes that further elaborate on why the formula couldn't be verified.

Overrides:

verifyFormula in class AbstractLTSminLTLMealy<I,O>

Parameters:

formula - the formula to verify