Package net.maswag.falcaun

Class StopDisprovedEQOracle.StaticLTLList<I>

java.lang.Object

net.maswag.falcaun.AbstractAdaptiveSTLUpdater<I>

net.maswag.falcaun.StopDisprovedEQOracle.StaticLTLList<I>

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>

Enclosing class:

StopDisprovedEQOracle<I,O,C>

public static class StopDisprovedEQOracle.StaticLTLList<I>
extends AbstractAdaptiveSTLUpdater<I>

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
(package private) List<String>	ltlProperties

Fields inherited from class net.maswag.falcaun.AbstractAdaptiveSTLUpdater

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

Constructor Summary

Constructors

Constructor	Description
StaticLTLList(List<String> ltlProperties)

Method Summary

Modifier and Type	Method	Description
boolean	allDisproved()	Checks if all the Signal Temporal Logic (STL) properties have been disproved.
@Nullable DefaultQuery<String,net.automatalib.word.Word<String>>	findCounterExample(@NotNull net.automatalib.automaton.transducer.MealyMachine<?,String,?,String> hypothesis, @NotNull Collection<? extends String> inputs)	Find a counter example using the current list of STL formulas
List<String>	getLTLProperties()	Returns the current list of Linear Temporal Logic (LTL) formulas in their string representations in LTSMin's syntax.
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.
int	size()	Returns the number of Signal Temporal Logic (STL) formulas in the current list.
Stream<PropertyOracle.MealyPropertyOracle<String,String,String>>	stream()	Returns a stream of property oracles used to verify the Signal Temporal Logic (STL) properties.

Methods inherited from class net.maswag.falcaun.AbstractAdaptiveSTLUpdater

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

getSTLProperties, list, setInputAlphabet

Methods inherited from interface de.learnlib.oracle.InclusionOracle

isCounterExample

Field Details

ltlProperties

List<String> ltlProperties

disprovedIndices

Set<Integer> disprovedIndices

Constructor Details

StaticLTLList

public StaticLTLList(List<String> ltlProperties)

Method Details

getLTLProperties

public List<String> getLTLProperties()

Description copied from interface: AdaptiveSTLUpdater

Returns the current list of Linear Temporal Logic (LTL) formulas in their string representations in LTSMin's syntax.

Returns:

A list of LTL properties as strings

size

public int size()

Description copied from interface: AdaptiveSTLUpdater

Returns the number of Signal Temporal Logic (STL) formulas in the current list.

Returns:

The number of STL formulas.

stream

public Stream<PropertyOracle.MealyPropertyOracle<String,String,String>> stream()

Description copied from class: AbstractAdaptiveSTLUpdater

Returns a stream of property oracles used to verify the Signal Temporal Logic (STL) properties.

Specified by:

stream in interface AdaptiveSTLUpdater<I>

Overrides:

stream in class AbstractAdaptiveSTLUpdater<I>

Returns:

A stream of PropertyOracle.MealyPropertyOracle instances.

findCounterExample

@Nullable
public @Nullable DefaultQuery<String,net.automatalib.word.Word<String>> findCounterExample(@NotNull
 @NotNull net.automatalib.automaton.transducer.MealyMachine<?,String,?,String> hypothesis,
 @NotNull
 @NotNull Collection<? extends String> inputs)

Find a counter example using the current list of STL formulas

Specified by:

findCounterExample in interface EquivalenceOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>

Overrides:

findCounterExample in class AbstractAdaptiveSTLUpdater<I>

Parameters:

hypothesis - The Mealy machine to be verified.

inputs - The alphabet of the Mealy machine's input symbols.

Returns:

A query representing a counterexample if one is found; otherwise, null.

See Also:

• ::findCounterExample

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.

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.

reset

public void reset()

Description copied from interface: AdaptiveSTLUpdater

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