Package net.maswag.falcaun

Class StaticSTLList<I>

java.lang.Object

net.maswag.falcaun.AbstractAdaptiveSTLUpdater<I>

net.maswag.falcaun.StaticSTLList<I>

Type Parameters:

I - Type of the input at each step.

All Implemented Interfaces:

de.learnlib.oracle.BlackBoxOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, de.learnlib.oracle.BlackBoxOracle.MealyBlackBoxOracle<String,String>, de.learnlib.oracle.EquivalenceOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, de.learnlib.oracle.EquivalenceOracle.MealyEquivalenceOracle<String,String>, de.learnlib.oracle.InclusionOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, de.learnlib.oracle.InclusionOracle.MealyInclusionOracle<String,String>, AdaptiveSTLUpdater<I>

public class StaticSTLList<I>
extends AbstractAdaptiveSTLUpdater<I>

List of STL/LTL formulas without update

Author:

Masaki Waga

See Also:

• BlackBoxVerifier
• NumericSULVerifier

Nested Class Summary

Nested classes/interfaces inherited from interface de.learnlib.oracle.BlackBoxOracle

de.learnlib.oracle.BlackBoxOracle.DFABlackBoxOracle<I>, de.learnlib.oracle.BlackBoxOracle.MealyBlackBoxOracle<I,O>

Nested classes/interfaces inherited from interface de.learnlib.oracle.EquivalenceOracle

de.learnlib.oracle.EquivalenceOracle.DFAEquivalenceOracle<I>, de.learnlib.oracle.EquivalenceOracle.MealyEquivalenceOracle<I,O>, de.learnlib.oracle.EquivalenceOracle.MooreEquivalenceOracle<I,O>

Nested classes/interfaces inherited from interface de.learnlib.oracle.InclusionOracle

de.learnlib.oracle.InclusionOracle.DFAInclusionOracle<I>, de.learnlib.oracle.InclusionOracle.MealyInclusionOracle<I,O>

Field Summary

Fields

Modifier and Type	Field	Description
(package private) Set<Integer>	disprovedIndices

Fields inherited from class net.maswag.falcaun.AbstractAdaptiveSTLUpdater

EDGE_PARSER, emptinessOracle, inclusionOracle, initialized, inputAlphabet, memOracle, modelChecker

Constructor Summary

Constructors

Constructor	Description
StaticSTLList()
StaticSTLList(Collection<? extends TemporalLogic<I>> STLProperties)
StaticSTLList(TemporalLogic<I> propertyOracle)

Method Summary

Modifier and Type	Method	Description
boolean	allDisproved()	Returns if all the properties are disproved
protected void	notifyFalsifiedProperty(List<Integer> falsifiedIndices)	Notify that this.getLTLProperties.get(i) is falsified by the currently learned model.
void	reset()	Reset the list of the STL formulas to the initial one.

Methods inherited from class net.maswag.falcaun.AbstractAdaptiveSTLUpdater

addSTLProperties, addSTLProperty, findCounterExample, getPropertyOracles, newlyFalsifiedFormula, removeSTLProperties, removeSTLProperty, setMemOracle, stream, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface net.maswag.falcaun.AdaptiveSTLUpdater

getLTLProperties, getSTLProperties, list, setInputAlphabet, size

Methods inherited from interface de.learnlib.oracle.InclusionOracle

isCounterExample

Field Details

disprovedIndices

Set<Integer> disprovedIndices

Constructor Details

StaticSTLList

public StaticSTLList()

StaticSTLList

public StaticSTLList(TemporalLogic<I> propertyOracle)

StaticSTLList

public StaticSTLList(Collection<? extends TemporalLogic<I>> STLProperties)

Method Details

allDisproved

public boolean allDisproved()

Description copied from interface: AdaptiveSTLUpdater

Returns if all the properties are disproved

notifyFalsifiedProperty

protected void notifyFalsifiedProperty(List<Integer> falsifiedIndices)

Description copied from class: AbstractAdaptiveSTLUpdater

Notify that this.getLTLProperties.get(i) is falsified by the currently learned model.

Typically, we can generate a new adaptive formula. Note: we should not remove the original formula by this.

Overrides:

notifyFalsifiedProperty in class AbstractAdaptiveSTLUpdater<I>

Parameters:

falsifiedIndices - The set of indices of the falsified LTL formulas

reset

public void reset()

Description copied from interface: AdaptiveSTLUpdater

Reset the list of the STL formulas to the initial one.