Uses of Interface
net.maswag.falcaun.parser.TemporalLogic

Packages that use TemporalLogic

Package	Description
net.maswag.falcaun	FalCAuN - Falsification tool for Cyber-Physical Systems via Automata Learning.
net.maswag.falcaun.parser	FalCAuN parser package: STL/LTL formula parsing, signal mapping, and temporal logic utilities.

Uses of TemporalLogic in net.maswag.falcaun

Fields in net.maswag.falcaun with type parameters of type TemporalLogic

Modifier and Type	Field	Description
private final List<List<TemporalLogic<I>>>	AdaptiveSTLList.candidateSTLProperties
private List<TemporalLogic<I>>	BlackBoxVerifier.cexProperty	A list of Signal Temporal Logic (STL) properties that were violated by the counterexamples found during the verification process.
private final List<TemporalLogic<I>>	AdaptiveSTLList.falsifiedSTLProperties
Function<TemporalLogic<I>,TemporalLogic<I>>	AdaptiveSTLList.IntervalTL.frame
Function<TemporalLogic<I>,TemporalLogic<I>>	AdaptiveSTLList.IntervalTL.frame
private final List<TemporalLogic<I>>	AdaptiveSTLList.initialSTLs
private final List<TemporalLogic<I>>	AbstractAdaptiveSTLUpdater.reportedFormulas	A list of Signal Temporal Logic (STL) formulas that have been disproved by the verification process.
private final List<TemporalLogic<I>>	AbstractAdaptiveSTLUpdater.STLProperties	A list of Signal Temporal Logic (STL) properties that need to be verified against the system.
private final List<List<TemporalLogic<I>>>	AdaptiveSTLList.strengthenedSTLProperties
private final List<TemporalLogic<I>>	AdaptiveSTLList.targetSTLs

Methods in net.maswag.falcaun that return TemporalLogic

Modifier and Type	Method	Description
TemporalLogic<I>	AdaptiveSTLList.IntervalTL.getOriginalSTL()
TemporalLogic<I>	AdaptiveSTLList.IntervalTL.nextStrengthenedSTL()	strengthen an STL formula by changing an interval
private TemporalLogic<I>	AdaptiveSTLList.nextStrengthenedSTL(int targetIdx)
TemporalLogic<I>	AdaptiveSTLList.IntervalTL.strengthInit()

Methods in net.maswag.falcaun that return types with arguments of type TemporalLogic

Modifier and Type	Method	Description
private List<TemporalLogic<I>>	AdaptiveSTLList.generateStrengthenedSTL(TemporalLogic<I> targetStl)	generate syntactically strengthened STL formulas
List<TemporalLogic<List<Double>>>	NumericSULVerifier.getCexProperty()	Returns the falsified STL formulas in the string representation.
List<TemporalLogic<I>>	AdaptiveSTLUpdater.getSTLProperties()	Returns the current list of Signal Temporal Logic (STL) formulas.
private List<TemporalLogic<I>>	AdaptiveSTLList.strengthenSTL(TemporalLogic<I> stl)	syntactically strengthen an STL/LTL formula

Methods in net.maswag.falcaun with parameters of type TemporalLogic

Modifier and Type	Method	Description
protected void	AbstractAdaptiveSTLUpdater.addSTLProperty(TemporalLogic<I> stl)	Adds a Signal Temporal Logic (STL) property to the list of properties to be verified.
private List<AdaptiveSTLList.IntervalTL<I>>	AdaptiveSTLList.findIntervalSTL(TemporalLogic<I> stl, Function<TemporalLogic<I>,TemporalLogic<I>> frame)	find intervals that can be strengthened
private List<TemporalLogic<I>>	AdaptiveSTLList.generateStrengthenedSTL(TemporalLogic<I> targetStl)	generate syntactically strengthened STL formulas
private List<AdaptiveSTLList.IntervalTL<I>>	AdaptiveSTLList.initializeIntervalSTLproperties(TemporalLogic<I> targetSTL)	list up intervals of temporal operators in target STL formulas that can be strengthened
final boolean	AbstractAdaptiveSTLUpdater.newlyFalsifiedFormula(TemporalLogic<I> stlFormula)	Checks if a given Signal Temporal Logic (STL) formula has been newly falsified.
boolean	AdaptiveSTLUpdater.newlyFalsifiedFormula(TemporalLogic<I> stlFormula)	Checks if a given Signal Temporal Logic (STL) formula has not yet been falsified.
private List<TemporalLogic<I>>	AdaptiveSTLList.strengthenSTL(TemporalLogic<I> stl)	syntactically strengthen an STL/LTL formula
String	AbstractAdaptiveSTLUpdater.toLTLString(TemporalLogic<I> prop)	Converts the given Temporal Logic property to its Linear Temporal Logic (LTL) string representation.
default String	AdaptiveSTLUpdater.toLTLString(TemporalLogic<I> prop)	Converts a given Signal Temporal Logic (STL) formula to its Linear Temporal Logic (LTL) string representation.

Method parameters in net.maswag.falcaun with type arguments of type TemporalLogic

Modifier and Type	Method	Description
protected void	AbstractAdaptiveSTLUpdater.addSTLProperties(Collection<? extends TemporalLogic<I>> stlCollection)	Adds a collection of Signal Temporal Logic (STL) properties to the list of properties to be verified.
private List<AdaptiveSTLList.IntervalTL<I>>	AdaptiveSTLList.findIntervalSTL(TemporalLogic<I> stl, Function<TemporalLogic<I>,TemporalLogic<I>> frame)	find intervals that can be strengthened
private List<AdaptiveSTLList.IntervalTL<I>>	AdaptiveSTLList.findIntervalSTL(TemporalLogic<I> stl, Function<TemporalLogic<I>,TemporalLogic<I>> frame)	find intervals that can be strengthened

Constructors in net.maswag.falcaun with parameters of type TemporalLogic

Modifier	Constructor	Description
	AdaptiveSTLList(TemporalLogic<I> propertyOracle)
	StaticSTLList(TemporalLogic<I> propertyOracle)

Constructor parameters in net.maswag.falcaun with type arguments of type TemporalLogic

Modifier	Constructor	Description
	AdaptiveSTLList(Collection<? extends TemporalLogic<I>> STLProperties)
	AdaptiveSTLList(Collection<? extends TemporalLogic<I>> STLProperties, int timeWindow)
	IntervalTL(TemporalSub<I> stl, Function<TemporalLogic<I>,TemporalLogic<I>> frame, int timeWindow)
	IntervalTL(TemporalSub<I> stl, Function<TemporalLogic<I>,TemporalLogic<I>> frame, int timeWindow)
	StaticSTLList(Collection<? extends TemporalLogic<I>> STLProperties)

Uses of TemporalLogic in net.maswag.falcaun.parser

Subinterfaces of TemporalLogic in net.maswag.falcaun.parser

Modifier and Type	Interface	Description
static interface	TemporalLogic.LTLFormula
static interface	TemporalLogic.STLCost

Classes in net.maswag.falcaun.parser that implement TemporalLogic

Modifier and Type	Class	Description
class	AbstractTemporalLogic<I>	Abstract base class for temporal logic formulas.
class	LTLAtomic	The atomic propositions in LTL formulas
class	STLAbstractAtomic	STLAtomic class.
class	STLInputAtomic	This class represents an atomic formula in STL for input signals.
class	STLOutputAtomic	STLAtomic class.
class	TemporalAnd<I>	The class representing the AND operator of temporal logic.
(package private) static class	TemporalAnd.LTLAnd
(package private) static class	TemporalAnd.STLAnd
class	TemporalConst<I>
(package private) static class	TemporalConst.LTLConst
(package private) static class	TemporalConst.STLConst
class	TemporalEventually<I>	STLEventually class.
(package private) static class	TemporalEventually.LTLEventually
(package private) static class	TemporalEventually.STLEventually
class	TemporalGlobally<I>	TemporalGlobally class.
(package private) static class	TemporalGlobally.LTLGlobally
static class	TemporalGlobally.STLGlobally
class	TemporalImply<I>	STLImply class.
(package private) static class	TemporalImply.LTLImply
static class	TemporalImply.STLImply
class	TemporalNext<I>	STLNext class.
(package private) static class	TemporalNext.LTLNext
static class	TemporalNext.STLNext
class	TemporalNot<I>	STLTemporalNot class.
(package private) static class	TemporalNot.LTLNot
(package private) static class	TemporalNot.STLNot
class	TemporalOp<I>
class	TemporalOr<I>	The class representing the OR operator of temporal logic.
(package private) static class	TemporalOr.LTLOr
(package private) static class	TemporalOr.STLOr
class	TemporalRelease<I>	TemporalRelease class.
(package private) static class	TemporalRelease.LTLRelease
(package private) static class	TemporalRelease.STLRelease
class	TemporalSub<I>
(package private) static class	TemporalSub.LTLSub
(package private) static class	TemporalSub.STLSub
class	TemporalUntil<I>	TemporalUntil class.
(package private) static class	TemporalUntil.LTLUntil
(package private) static class	TemporalUntil.STLUntil

Fields in net.maswag.falcaun.parser declared as TemporalLogic

Modifier and Type	Field	Description
private final TemporalLogic<I>	TemporalRelease.left
private final TemporalLogic<I>	TemporalUntil.left
private final TemporalLogic<I>	TemporalRelease.right
private final TemporalLogic<I>	TemporalUntil.right
private final TemporalLogic<I>	TemporalNext.subFml
protected final TemporalLogic<I>	TemporalNot.subFml
(package private) TemporalLogic<I>	TemporalOp.subFml
protected final TemporalLogic<I>	TemporalImply.subFml1
protected final TemporalLogic<I>	TemporalImply.subFml2

Fields in net.maswag.falcaun.parser with type parameters of type TemporalLogic

Modifier and Type	Field	Description
private final List<TemporalLogic<I>>	TemporalOr.subFmls
private final List<TemporalLogic<I>>	TemporalAnd.subFormulas

Methods in net.maswag.falcaun.parser that return TemporalLogic

Modifier and Type	Method	Description
TemporalLogic<I>	TemporalConst.derivativeOn(String c)
TemporalLogic<I>	TemporalEventually.getSubFml()	getSubFml.
TemporalLogic<I>	TemporalGlobally.getSubFml()	Get the sub-formula
TemporalLogic<I>	TemporalAnd.toDisjunctiveForm()
TemporalLogic<I>	TemporalConst.toDisjunctiveForm()
TemporalLogic<I>	TemporalEventually.toDisjunctiveForm()
TemporalLogic<I>	TemporalGlobally.toDisjunctiveForm()
TemporalLogic<I>	TemporalImply.toDisjunctiveForm()
TemporalLogic<I>	TemporalLogic.toDisjunctiveForm()
TemporalLogic<I>	TemporalNext.toDisjunctiveForm()
TemporalLogic<I>	TemporalNot.toDisjunctiveForm()
TemporalLogic<I>	TemporalOr.toDisjunctiveForm()
TemporalLogic<I>	TemporalRelease.toDisjunctiveForm()
TemporalLogic<I>	TemporalSub.toDisjunctiveForm()
TemporalLogic<I>	TemporalUntil.toDisjunctiveForm()
TemporalLogic<I>	TemporalAnd.toNnf(boolean negate)
TemporalLogic<I>	TemporalConst.toNnf(boolean negate)
TemporalLogic<I>	TemporalEventually.toNnf(boolean negate)
TemporalLogic<I>	TemporalGlobally.toNnf(boolean negate)
TemporalLogic<I>	TemporalImply.toNnf(boolean negate)
TemporalLogic<I>	TemporalLogic.toNnf(boolean neg)
TemporalLogic<I>	TemporalNext.toNnf(boolean negate)
TemporalLogic<I>	TemporalNot.toNnf(boolean negate)
TemporalLogic<I>	TemporalOr.toNnf(boolean negate)
TemporalLogic<I>	TemporalRelease.toNnf(boolean negate)
TemporalLogic<I>	TemporalSub.toNnf(boolean negate)
TemporalLogic<I>	TemporalUntil.toNnf(boolean negate)

Methods in net.maswag.falcaun.parser that return types with arguments of type TemporalLogic

Modifier and Type	Method	Description
List<TemporalLogic<String>>	LTLAtomic.getAllConjunctions()
List<TemporalLogic<List<Double>>>	STLInputAtomic.getAllConjunctions()
List<TemporalLogic<List<Double>>>	STLOutputAtomic.getAllConjunctions()
List<TemporalLogic<I>>	TemporalAnd.getAllConjunctions()
List<TemporalLogic<I>>	TemporalConst.getAllConjunctions()
List<TemporalLogic<I>>	TemporalEventually.getAllConjunctions()
List<TemporalLogic<I>>	TemporalGlobally.getAllConjunctions()
List<TemporalLogic<I>>	TemporalImply.getAllConjunctions()
List<TemporalLogic<I>>	TemporalLogic.getAllConjunctions()
List<TemporalLogic<I>>	TemporalNext.getAllConjunctions()
List<TemporalLogic<I>>	TemporalNot.getAllConjunctions()
List<TemporalLogic<I>>	TemporalOr.getAllConjunctions()
List<TemporalLogic<I>>	TemporalRelease.getAllConjunctions()
List<TemporalLogic<I>>	TemporalSub.getAllConjunctions()
List<TemporalLogic<I>>	TemporalUntil.getAllConjunctions()

Method parameters in net.maswag.falcaun.parser with type arguments of type TemporalLogic

Modifier and Type	Method	Description
private static void	LTLFormulaHelper.handleMultiaryOperator(Iterable<? extends TemporalLogic<?>> subFormulas, LTLAPs aps)	Handles multiary operators (operators with multiple subformulas).

Constructors in net.maswag.falcaun.parser with parameters of type TemporalLogic

Modifier	Constructor	Description
(package private)	LTLOr(TemporalLogic<String> subFml1, TemporalLogic<String> subFml2)
(package private)	LTLUntil(TemporalLogic<String> left, TemporalLogic<String> right)
	TemporalAnd(TemporalLogic<I> subFml1, TemporalLogic<I> subFml2)
	TemporalEventually(TemporalLogic<I> subFml)
	TemporalGlobally(TemporalLogic<I> subFml)
(package private)	TemporalImply(TemporalLogic<I> subFml1, TemporalLogic<I> subFml2)
(package private)	TemporalNext(TemporalLogic<I> subFml, boolean nullPositive)
(package private)	TemporalNot(TemporalLogic<I> subFml)	Constructs a new TemporalNot with the specified sub formula.
(package private)	TemporalOp(TemporalLogic<I> subFml)
	TemporalOr(TemporalLogic<I> subFml1, TemporalLogic<I> subFml2)
(package private)	TemporalRelease(TemporalLogic<I> left, TemporalLogic<I> right)
(package private)	TemporalUntil(TemporalLogic<I> left, TemporalLogic<I> right)

Constructor parameters in net.maswag.falcaun.parser with type arguments of type TemporalLogic

Modifier	Constructor	Description
(package private)	LTLAnd(List<TemporalLogic<String>> subFormulas)
(package private)	STLAnd(List<TemporalLogic<List<Double>>> subFormulas)
	TemporalAnd(List<TemporalLogic<I>> subFormulas)
	TemporalOr(List<TemporalLogic<I>> subFmls)