Package net.maswag.falcaun.parser

Class LTLFormulaHelper

java.lang.Object

net.maswag.falcaun.parser.LTLFormulaHelper

public class LTLFormulaHelper
extends Object

Helper class for LTL formula operations.

Constructor Summary

Constructors

Constructor	Description
LTLFormulaHelper()

Method Summary

Modifier and Type	Method	Description
static LTLAPs	collectAPs(TemporalLogic.LTLFormula formula)	Collects all atomic propositions from a formula tree and creates an APs collection.
private static void	collectAtomicPropositionsRecursive(Object formula, LTLAPs aps)
static List<TemporalLogic.LTLFormula>	convertToLTLFormulas(List<TemporalLogic.STLCost> stlFormulas)	Converts a list of STL formulas to prepared LTL formulas.
private static void	handleAtomicFormula(LTLAtomic atomic, LTLAPs aps)	Handles atomic formulas by collecting their atomic propositions.
private static void	handleBinaryOperator(Object leftFormula, Object rightFormula, LTLAPs aps)	Handles binary operators (operators with two subformulas).
private static void	handleMultiaryOperator(Iterable<? extends TemporalLogic<?>> subFormulas, LTLAPs aps)	Handles multiary operators (operators with multiple subformulas).
private static void	handleUnaryOperator(Object subFormula, LTLAPs aps)	Handles unary operators (operators with a single subformula).
static TemporalLogic.LTLFormula	prepareFormula(TemporalLogic.LTLFormula formula)	Prepares a formula for use by collecting its atomic propositions and setting them.
static void	setAPs(TemporalLogic.LTLFormula formula, LTLAPs aps)	Sets the atomic propositions on a formula tree and propagates it to all subformulas.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

LTLFormulaHelper

public LTLFormulaHelper()

Method Details

collectAPs

public static LTLAPs collectAPs(TemporalLogic.LTLFormula formula)

Collects all atomic propositions from a formula tree and creates an APs collection.

Parameters:

formula - The root formula

Returns:

An LTLAPs containing all atomic propositions found in the formula

setAPs

public static void setAPs(TemporalLogic.LTLFormula formula,
 LTLAPs aps)

Sets the atomic propositions on a formula tree and propagates it to all subformulas.

Parameters:

formula - The root formula

aps - The atomic propositions to set

prepareFormula

public static TemporalLogic.LTLFormula prepareFormula(TemporalLogic.LTLFormula formula)

Prepares a formula for use by collecting its atomic propositions and setting them.

Parameters:

formula - The formula to prepare

Returns:

The same formula with atomic propositions set

collectAtomicPropositionsRecursive

private static void collectAtomicPropositionsRecursive(Object formula,
 LTLAPs aps)

handleAtomicFormula

private static void handleAtomicFormula(LTLAtomic atomic,
 LTLAPs aps)

Handles atomic formulas by collecting their atomic propositions.

handleUnaryOperator

private static void handleUnaryOperator(Object subFormula,
 LTLAPs aps)

Handles unary operators (operators with a single subformula).

handleBinaryOperator

private static void handleBinaryOperator(Object leftFormula,
 Object rightFormula,
 LTLAPs aps)

Handles binary operators (operators with two subformulas).

handleMultiaryOperator

private static void handleMultiaryOperator(Iterable<? extends TemporalLogic<?>> subFormulas,
 LTLAPs aps)

Handles multiary operators (operators with multiple subformulas).

convertToLTLFormulas

public static List<TemporalLogic.LTLFormula> convertToLTLFormulas(List<TemporalLogic.STLCost> stlFormulas)

Converts a list of STL formulas to prepared LTL formulas.

Parameters:

stlFormulas - The list of STL formulas to convert

Returns:

A list of prepared LTL formulas with atomic propositions set

Throws:

IllegalArgumentException - if stlFormulas is null