Package net.maswag.falcaun

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, 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.

    • 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.
      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.

    • constructSatisfyingAtomicPropositions

      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.

    • getIOType

      @Nonnull TemporalLogic.IOType getIOType()

    • getSatisfyingAtomicPropositions

      @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.