Package net.maswag.falcaun

Class AdaptiveSTLList<I>

java.lang.Object

net.maswag.falcaun.AbstractAdaptiveSTLUpdater<I>

net.maswag.falcaun.AdaptiveSTLList<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 AdaptiveSTLList<I>
extends AbstractAdaptiveSTLUpdater<I>

Adaptive updater of STL/LTL formulas

Author:

Junya Shijubo

See Also:

• BlackBoxVerifier
• NumericSULVerifier

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
private static class	AdaptiveSTLList.IntervalTL<I>

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
private final List<List<TemporalLogic<I>>>	candidateSTLProperties
private final List<TemporalLogic<I>>	falsifiedSTLProperties
private final List<TemporalLogic<I>>	initialSTLs
private final List<List<AdaptiveSTLList.IntervalTL<I>>>	intervalSTLProperties
private final List<List<TemporalLogic<I>>>	strengthenedSTLProperties
private final List<TemporalLogic<I>>	targetSTLs
private final int	timeWindow

Fields inherited from class net.maswag.falcaun.AbstractAdaptiveSTLUpdater

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

Constructor Summary

Constructors

Constructor	Description
AdaptiveSTLList()
AdaptiveSTLList(Collection<? extends TemporalLogic<I>> STLProperties)
AdaptiveSTLList(Collection<? extends TemporalLogic<I>> STLProperties, int timeWindow)
AdaptiveSTLList(TemporalLogic<I> propertyOracle)

Method Summary

Modifier and Type	Method	Description
boolean	allDisproved()	Returns if all the properties are disproved
private List<AdaptiveSTLList.IntervalTL<I>>	findIntervalSTL(TemporalLogic<I> stl, Function<TemporalLogic<I>,TemporalLogic<I>> frame)	find intervals that can be strengthened
private List<TemporalLogic<I>>	generateStrengthenedSTL(TemporalLogic<I> targetStl)	generate syntactically strengthened STL formulas
private List<AdaptiveSTLList.IntervalTL<I>>	initializeIntervalSTLproperties(TemporalLogic<I> targetSTL)	list up intervals of temporal operators in target STL formulas that can be strengthened
private TemporalLogic<I>	nextStrengthenedSTL(int targetIdx)
protected void	notifyFalsifiedProperty(List<Integer> falsifiedIndices)	Notify that subset of this.getLTLProperties are falsified by the currently learned model.
void	reset()	Remove all the non-initial STL formulas
private List<TemporalLogic<I>>	strengthenSTL(TemporalLogic<I> stl)	syntactically strengthen an STL/LTL formula

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

initialSTLs

private final List<TemporalLogic<I>> initialSTLs

targetSTLs

private final List<TemporalLogic<I>> targetSTLs

strengthenedSTLProperties

private final List<List<TemporalLogic<I>>> strengthenedSTLProperties

candidateSTLProperties

private final List<List<TemporalLogic<I>>> candidateSTLProperties

intervalSTLProperties

private final List<List<AdaptiveSTLList.IntervalTL<I>>> intervalSTLProperties

falsifiedSTLProperties

private final List<TemporalLogic<I>> falsifiedSTLProperties

timeWindow

private final int timeWindow

Constructor Details

AdaptiveSTLList

public AdaptiveSTLList()

AdaptiveSTLList

public AdaptiveSTLList(TemporalLogic<I> propertyOracle)

AdaptiveSTLList

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

AdaptiveSTLList

public AdaptiveSTLList(Collection<? extends TemporalLogic<I>> STLProperties,
 int timeWindow)

Parameters:

STLProperties - The list of STL/LTL formulas to verify

timeWindow - The maximum time window of the STL formulas. This is typically the number of steps in each simulation.

Method Details

strengthenSTL

private List<TemporalLogic<I>> strengthenSTL(TemporalLogic<I> stl)

syntactically strengthen an STL/LTL formula

Parameters:

stl - a target STL formula to be strengthen

Returns:

list of TemporalLogic<I> objects

notifyFalsifiedProperty

protected void notifyFalsifiedProperty(List<Integer> falsifiedIndices)

Notify that subset of this.getLTLProperties are falsified by the currently learned model.

Overrides:

notifyFalsifiedProperty in class AbstractAdaptiveSTLUpdater<I>

Parameters:

falsifiedIndices - The set of indices of the falsified LTL formulas

generateStrengthenedSTL

private List<TemporalLogic<I>> generateStrengthenedSTL(TemporalLogic<I> targetStl)

generate syntactically strengthened STL formulas

Parameters:

targetStl - a target STL/LTL formula

Returns:

list of strengthened formulas

initializeIntervalSTLproperties

private List<AdaptiveSTLList.IntervalTL<I>> initializeIntervalSTLproperties(TemporalLogic<I> targetSTL)

list up intervals of temporal operators in target STL formulas that can be strengthened

Parameters:

targetSTL - a target STL/LTL formula

Returns:

list of

findIntervalSTL

private List<AdaptiveSTLList.IntervalTL<I>> findIntervalSTL(TemporalLogic<I> stl,
 Function<TemporalLogic<I>,TemporalLogic<I>> frame)

find intervals that can be strengthened

Parameters:

stl - target STL formula

frame - outer frame of param 'stl'

Returns:

list of AdaptiveSTLList.IntervalTL object

nextStrengthenedSTL

private TemporalLogic<I> nextStrengthenedSTL(int targetIdx)

allDisproved

public boolean allDisproved()

Description copied from interface: AdaptiveSTLUpdater

Returns if all the properties are disproved

reset

public void reset()

Remove all the non-initial STL formulas