Package net.maswag.falcaun.parser

Class STLOutputAtomic

java.lang.Object
net.maswag.falcaun.parser.AbstractTemporalLogic<List<Double>>
net.maswag.falcaun.parser.STLAbstractAtomic
net.maswag.falcaun.parser.STLOutputAtomic
All Implemented Interfaces:
Function<IOSignal<List<Double>>,Double>, TemporalLogic<List<Double>>, TemporalLogic.STLCost
public class STLOutputAtomic extends STLAbstractAtomic

STLAtomic class.

This class represents an atomic formula in STL for output signals. This class has the functions to construct the atomic propositions, a set of alphabets representing the output signal, from the atomic formula and its output mapper. For example, let an atomic formula be output(0) > 1.0, the 0-th output mapper be {a: 1.0, b: 2.0, c: 3.0}, the 0-th largest be 'd', the set of alphabets of 1st output signal be {'x', 'y'}, and the 1st largest be 'z', then the atomic propositions are {"bx", "by", "bz", "cx", "cy", "cz", "dx", "dy", "dz"}.

When the 0-th output mapper is {a: 1.0, b: 2.0, c: 3.0} and largest is {'d'}, the comparator in ranges of (-inf, 1.0], (1.0, 2.0], (2.0, 3.0] is mapped to 'a', 'b', 'c' for each and those in the range (3.0, +inf) are mapped to 'd'.

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

  • Field Details

  • Constructor Details

    • STLOutputAtomic

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

      Constructor for STLOutputAtomic.

      Constructs an atomic proposition output(sigIndex) op comparator.
      Parameters:
      sigIndex - An index of output 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. largest is also used to construct the atomic propositions.
      Specified by:
      constructAllAPs in class STLAbstractAtomic
      Parameters:
      index - The index of the signal

    • setOutputMaps

      private void setOutputMaps()

    • setMapper

      void setMapper(OutputMapper mapper)

    • setAtomic

      public void setAtomic(List<Map<Character,Double>> outputMapper, List<Character> largest)

    • setOutputMapper

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

    • setLargest

      void setLargest(List<Character> largest)
      Gives the largest alphabets for the atomic formula. It is required to construct the atomic propositions.
      Parameters:
      largest - The list of largest characters 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()