Package net.maswag.falcaun.parser

Class STLInputAtomic

java.lang.Object
net.maswag.falcaun.parser.AbstractTemporalLogic<List<Double>>
net.maswag.falcaun.parser.STLAbstractAtomic
net.maswag.falcaun.parser.STLInputAtomic
All Implemented Interfaces:
Function<IOSignal<List<Double>>,Double>, TemporalLogic<List<Double>>, TemporalLogic.STLCost
public class STLInputAtomic extends STLAbstractAtomic
This class represents an atomic formula in STL for input signals. This class has the functions to construct the atomic propositions, a set of alphabets representing the input signal, from the atomic formula and its input mapper. For example, let an atomic formula be input(0) > 1.0, the 0-th input mapper be {a: 1.0, b: 2.0, c: 3.0}, and the set of alphabets of 1st input signal be {'x', 'y'}, then the atomic propositions are {"bx", "by", "cx", "cy"}.

When the 0-th input mapper is {a: 1.0, b: 2.0, c: 3.0},

  • Given input(0) < 1.0, the satisfying 0-th alphabets are {'a'}. Note that < (Operation.lt) represents a less-than-or-equal-to operator.
  • Given input(0) == 1.5, getAllAPs() raises a RuntimeException.
Author:
Masaki Waga <masakiwaga@gmail.com>

  • Field Details

  • Constructor Details

    • STLInputAtomic

      public STLInputAtomic(int sigIndex, STLAbstractAtomic.Operation op, double comparator)

      Constructor for STLInputAtomic.

      Constructs an atomic proposition input(sigIndex) op comparator.
      Parameters:
      sigIndex - An index of input signals
      op - The comparison operator STLAbstractAtomic.Operation
      comparator - The value to compare against

  • Method Details

    • 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

    • constructSatisfyingAtomicPropositions

      public void constructSatisfyingAtomicPropositions()
      Constructs AbstractTemporalLogic.satisfyingAtomicPropositions if not initialized.

    • constructSmallerAPs

      protected Set<Character> constructSmallerAPs(int index, double threshold)
      Constructs a set of characters representing atomic propositions that are smaller than the given threshold for the specified signal index.
      Specified by:
      constructSmallerAPs in class STLAbstractAtomic
      Parameters:
      index - The index of the signal.
      Returns:
      A set of characters representing the atomic propositions.

    • constructLargerAPs

      protected Set<Character> constructLargerAPs(int index, double threshold)
      Constructs a set of characters representing atomic propositions that are greater than the given threshold for the specified signal index.
      Specified by:
      constructLargerAPs in class STLAbstractAtomic
      Parameters:
      index - The index of the signal.
      Returns:
      A set of characters representing the atomic propositions.

    • constructEqAPs

      protected Set<Character> constructEqAPs(int index, double threshold)
      Constructs a set of characters representing atomic propositions that are equal to the given threshold for the specified signal index.
      Specified by:
      constructEqAPs in class STLAbstractAtomic
      Parameters:
      index - The index of the signal.
      Returns:
      A set of characters representing the atomic propositions.

    • constructAllAPs

      protected Set<Character> constructAllAPs(int index)
      Construct the characters that represent the abstract values of the signal.
      Specified by:
      constructAllAPs in class STLAbstractAtomic
      Parameters:
      index - The index of the signal

    • setInputMaps

      private void setInputMaps()

    • setInputMapper

      void setInputMapper(List<Map<Character,Double>> inputMapper)
      Gives the input mapper for the atomic formula. It is required to construct the atomic propositions.
      Parameters:
      inputMapper - The input mapper to set

    • getRoSI

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

    • getSignalName

      protected String getSignalName()
      Specified by:
      getSignalName in class STLAbstractAtomic

    • toNnf

      public TemporalLogic.STLCost toNnf(boolean negate)

    • toDisjunctiveForm

      public TemporalLogic.STLCost toDisjunctiveForm()

    • getAllConjunctions

      public List<TemporalLogic<List<Double>>> getAllConjunctions()