Package net.maswag.falcaun.parser

Class LTLAtomic

java.lang.Object

net.maswag.falcaun.parser.AbstractTemporalLogic<String>

net.maswag.falcaun.parser.LTLAtomic

All Implemented Interfaces:

Function<IOSignal<String>,Double>, TemporalLogic<String>, TemporalLogic.LTLFormula

public class LTLAtomic
extends AbstractTemporalLogic<String>
implements TemporalLogic.LTLFormula

The atomic propositions in LTL formulas

Nested Class Summary

Nested classes/interfaces inherited from interface net.maswag.falcaun.parser.TemporalLogic

TemporalLogic.IOType, TemporalLogic.LTLFormula, TemporalLogic.STLCost

Field Summary

Fields

Modifier and Type	Field	Description
private final LTLFormulaBase	formulaBase
private final Optional<String>	inputString
private final Optional<String>	outputString

Fields inherited from class net.maswag.falcaun.parser.AbstractTemporalLogic

initialized, iOType, nonTemporal, satisfyingAtomicPropositions

Constructor Summary

Constructors

Constructor	Description
LTLAtomic(Optional<String> inputString, Optional<String> outputString)

Method Summary

Modifier and Type	Method	Description
void	collectAtomicPropositions(LTLAPs aps)	Collects all atomic propositions from this formula and its subformulas.
void	constructSatisfyingAtomicPropositions()
Set<String>	getAllAPs()	Returns all atomic propositions from the appropriate set based on the IO type.
List<TemporalLogic<String>>	getAllConjunctions()
LTLAPs	getAPs()	Gets the atomic propositions for this formula.
RoSI	getRoSI(IOSignal<String> signal)	Evaluate the formula on the given signal and returns the RoSI, i.e., the range of the possible robustness values after concatenating a suffix.
void	setAPs(LTLAPs aps)	Sets the universe of atomic propositions for this formula.
String	toAbstractLTLString(Map<String,String> mapper)
String	toAbstractString()	Returns a string representation of the formula in the format of LTSMin.
TemporalLogic.LTLFormula	toDisjunctiveForm()
TemporalLogic.LTLFormula	toNnf(boolean negate)
String	toOwlString()
String	toString()

Methods inherited from class net.maswag.falcaun.parser.AbstractTemporalLogic

equals, getSatisfyingAtomicPropositions, hashCode, makeAbstractStringWithAtomicStrings, makeAbstractStringWithAtomicStrings

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.util.function.Function

andThen, compose

Methods inherited from interface net.maswag.falcaun.parser.TemporalLogic

apply, getIOType, getSatisfyingAtomicPropositions, isInitialized, isNonTemporal, toLTLString

Field Details

formulaBase

private final LTLFormulaBase formulaBase

inputString

private final Optional<String> inputString

outputString

private final Optional<String> outputString

Constructor Details

LTLAtomic

public LTLAtomic(Optional<String> inputString,
 Optional<String> outputString)

Method Details

setAPs

public void setAPs(LTLAPs aps)

Sets the universe of atomic propositions for this formula. This is necessary for correctly computing negation.

Specified by:

setAPs in interface TemporalLogic.LTLFormula

Parameters:

aps - The atomic propositions containing all possible input and output APs

getAPs

public LTLAPs getAPs()

Gets the atomic propositions for this formula.

Specified by:

getAPs in interface TemporalLogic.LTLFormula

Returns:

The atomic propositions, or null if not set

getAllAPs

public Set<String> getAllAPs()

Returns all atomic propositions from the appropriate set based on the IO type. Requires that APs have been set via setAPs() before calling this method.

Specified by:

getAllAPs in interface TemporalLogic<String>

Returns:

Set of atomic propositions based on the IO type (input, output, or both)

Throws:

IllegalStateException - if APs have not been set

collectAtomicPropositions

public void collectAtomicPropositions(LTLAPs aps)

Description copied from interface: TemporalLogic.LTLFormula

Collects all atomic propositions from this formula and its subformulas.

Specified by:

collectAtomicPropositions in interface TemporalLogic.LTLFormula

Parameters:

aps - The atomic propositions to populate

constructSatisfyingAtomicPropositions

public void constructSatisfyingAtomicPropositions()

Specified by:

constructSatisfyingAtomicPropositions in interface TemporalLogic<String>

toAbstractString

public String toAbstractString()

Description copied from interface: TemporalLogic

Returns a string representation of the formula in the format of LTSMin.

Specified by:

toAbstractString in interface TemporalLogic<String>

Returns:

a String object representing the formula in the format of LTSMin.

toString

public String toString()

Overrides:

toString in class Object

toAbstractLTLString

public String toAbstractLTLString(Map<String,String> mapper)

Specified by:

toAbstractLTLString in interface TemporalLogic<String>

toOwlString

public String toOwlString()

Specified by:

toOwlString in interface TemporalLogic<String>

getRoSI

public RoSI getRoSI(IOSignal<String> signal)

Description copied from interface: TemporalLogic

Evaluate the formula on the given signal and returns the RoSI, i.e., the range of the possible robustness values after concatenating a suffix.

Specified by:

getRoSI in interface TemporalLogic<String>

Parameters:

signal - The input-output signal to evaluate the formula on

Returns:

a RoSI object representing the range of the possible robustness values after concatenating a suffix.

toNnf

public TemporalLogic.LTLFormula toNnf(boolean negate)

Specified by:

toNnf in interface TemporalLogic<String>

toDisjunctiveForm

public TemporalLogic.LTLFormula toDisjunctiveForm()

Specified by:

toDisjunctiveForm in interface TemporalLogic<String>

getAllConjunctions

public List<TemporalLogic<String>> getAllConjunctions()

Specified by:

getAllConjunctions in interface TemporalLogic<String>