Package net.maswag.falcaun.parser

Interface TemporalLogic<I>

Type Parameters:
I - Type of the input at each step
All Superinterfaces:
Function<IOSignal<I>,Double>
All Known Subinterfaces:
TemporalLogic.LTLFormula, TemporalLogic.STLCost
All Known Implementing Classes:
AbstractTemporalLogic, LTLAtomic, STLAbstractAtomic, STLInputAtomic, STLOutputAtomic, TemporalAnd, TemporalAnd.LTLAnd, TemporalAnd.STLAnd, TemporalConst, TemporalConst.LTLConst, TemporalConst.STLConst, TemporalEventually, TemporalEventually.LTLEventually, TemporalEventually.STLEventually, TemporalGlobally, TemporalGlobally.LTLGlobally, TemporalGlobally.STLGlobally, TemporalImply, TemporalImply.LTLImply, TemporalImply.STLImply, TemporalNext, TemporalNext.LTLNext, TemporalNext.STLNext, TemporalNot, TemporalNot.LTLNot, TemporalNot.STLNot, TemporalOp, TemporalOr, TemporalOr.LTLOr, TemporalOr.STLOr, TemporalRelease, TemporalRelease.LTLRelease, TemporalRelease.STLRelease, TemporalSub, TemporalSub.LTLSub, TemporalSub.STLSub, TemporalUntil, TemporalUntil.LTLUntil, TemporalUntil.STLUntil
public interface TemporalLogic<I> extends Function<IOSignal<I>,Double>

Interface of a TemporalLogic formula.

Author:
Masaki Waga <masakiwaga@gmail.com>

  • Method Details

    • toAbstractString

      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.

    • toLTLString

      default String toLTLString()
      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

      String toAbstractLTLString(Map<String,String> mapper)

    • toOwlString

      String toOwlString()

    • getRoSI

      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.

    • apply

      default Double apply(IOSignal<I> signal)
      Evaluate the formula on the given signal and returns the robustness value.
      Specified by:
      apply in interface Function<IOSignal<I>,Double>

    • getAllAPs

      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

    • constructSatisfyingAtomicPropositions

      default void constructSatisfyingAtomicPropositions()

    • isNonTemporal

      boolean isNonTemporal()
      Returns true if the formula does not contain any temporal operators.
      Returns:
      a boolean value indicating whether the formula contains any temporal operators.

    • isInitialized

      boolean isInitialized()
      Returns true if the mapper is set.
      Returns:
      true if the formula is initialized with a mapper, false otherwise

    • getIOType

      @NotNull @NotNull TemporalLogic.IOType getIOType()

    • getSatisfyingAtomicPropositions

      @Nullable @Nullable Collection<String> getSatisfyingAtomicPropositions()
      Returns the collection of atomic propositions such that if one of them is satisfied, the formula is satisfied. If there is no such collection, returns null

      Such a set exists if the formula does not contain any temporal operators.

      Returns:
      A collection of atomic propositions that satisfy the formula, or null if no such collection exists

    • toNnf

      TemporalLogic<I> toNnf(boolean neg)

    • toDisjunctiveForm

      TemporalLogic<I> toDisjunctiveForm()

    • getAllConjunctions

      List<TemporalLogic<I>> getAllConjunctions()