Package net.maswag.falcaun.parser

Class TemporalUntil<I>

java.lang.Object
net.maswag.falcaun.parser.AbstractTemporalLogic<I>
net.maswag.falcaun.parser.TemporalUntil<I>
Type Parameters:
I - Type of the input at each step
All Implemented Interfaces:
Function<IOSignal<I>,Double>, TemporalLogic<I>
Direct Known Subclasses:
TemporalUntil.LTLUntil, TemporalUntil.STLUntil
public class TemporalUntil<I> extends AbstractTemporalLogic<I>

TemporalUntil class.

This class implements the until operator in STL and LTL.

Author:
Masaki Waga <masakiwaga@gmail.com>

  • Field Details

  • Constructor Details

  • Method Details

    • getRoSI

      public RoSI getRoSI(IOSignal<I> 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.
      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.

    • getRoSIRaw

      public RoSI getRoSIRaw(IOSignal<I> signal)

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • constructSatisfyingAtomicPropositions

      public void constructSatisfyingAtomicPropositions()

    • getAllAPs

      public Set<String> getAllAPs()
      Returns the collection of atomic propositions under consideration. If this formula contains only the input constraints, the atomic propositions are the input constraints. If this formula contains only the output constraints, the atomic propositions are the output constraints. If this formula contains both input and output constraints, the atomic propositions are one of the input and output constraints.
      Returns:
      A set of all atomic propositions in the formula

    • toAbstractString

      public String toAbstractString()
      Returns a string representation of the formula in the format of LTSMin.
      Returns:
      a String object representing the formula in the format of LTSMin.

    • toAbstractLTLString

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

    • toOwlString

      public String toOwlString()

    • toNnf

      public TemporalLogic<I> toNnf(boolean negate)

    • toDisjunctiveForm

      public TemporalLogic<I> toDisjunctiveForm()

    • getAllConjunctions

      public List<TemporalLogic<I>> getAllConjunctions()