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:

BlackBoxOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, BlackBoxOracle.MealyBlackBoxOracle<String,String>, EquivalenceOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, EquivalenceOracle.MealyEquivalenceOracle<String,String>, InclusionOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, 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

BlackBoxOracle.DFABlackBoxOracle<I extends Object>, BlackBoxOracle.MealyBlackBoxOracle<I extends Object,O extends Object>

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

EquivalenceOracle.DFAEquivalenceOracle<I extends Object>, EquivalenceOracle.MealyEquivalenceOracle<I extends Object,O extends Object>, EquivalenceOracle.MooreEquivalenceOracle<I extends Object,O extends Object>

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

InclusionOracle.DFAInclusionOracle<I extends Object>, InclusionOracle.MealyInclusionOracle<I extends Object,O extends Object>

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()	Checks if all the Signal Temporal Logic (STL) properties have been disproved.
protected void	notifyFalsifiedProperty(List<Integer> falsifiedIndices)	Notifies that the STL properties at the specified indices are falsified by the currently learned model.
void	reset()	Resets the list of Signal Temporal Logic (STL) formulas to their initial state.

Methods inherited from class net.maswag.falcaun.AbstractAdaptiveSTLUpdater

addSTLProperties, addSTLProperty, findCounterExample, getPropertyOracles, newlyFalsifiedFormula, removeSTLProperties, removeSTLProperty, setMapper, setMemOracle, stream, toLTLString, 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

Checks if all the Signal Temporal Logic (STL) properties have been disproved.

Returns:

true if all STL properties have been disproved, otherwise false.

notifyFalsifiedProperty

protected void notifyFalsifiedProperty(List<Integer> falsifiedIndices)

Description copied from class: AbstractAdaptiveSTLUpdater

Notifies that the STL properties at the specified indices are falsified by the currently learned model.

This method is called when one or more STL properties have been disproved. It allows for generating new adaptive formulas based on these falsifications. Note: The original formulas should not be removed; instead, they can be adapted or extended.

Overrides:

notifyFalsifiedProperty in class AbstractAdaptiveSTLUpdater<I>

Parameters:

falsifiedIndices - A list of indices corresponding to the falsified STL properties.

reset

public void reset()

Description copied from interface: AdaptiveSTLUpdater

Resets the list of Signal Temporal Logic (STL) formulas to their initial state.