Package net.maswag.falcaun

Class AbstractAdaptiveSTLUpdater<I>

java.lang.Object
net.maswag.falcaun.AbstractAdaptiveSTLUpdater<I>
Type Parameters:
I - Type of the input at each step
All Implemented Interfaces:
BlackBoxOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, BlackBoxOracle.MealyBlackBoxOracle<String,String>, EquivalenceOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, EquivalenceOracle.MealyEquivalenceOracle<String,String>, InclusionOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, InclusionOracle.MealyInclusionOracle<String,String>, AdaptiveSTLUpdater<I>
Direct Known Subclasses:
AdaptiveSTLList, StaticSTLList, StopDisprovedEQOracle.StaticLTLList
public abstract class AbstractAdaptiveSTLUpdater<I> extends Object implements AdaptiveSTLUpdater<I>
Abstract class representing a potentially adaptive set of Signal Temporal Logic (STL) formulas. This class provides a framework for updating and verifying STL properties in a system, allowing for dynamic adaptation based on new information or changes in the system's behavior.
Author:
Masaki Waga
See Also:

  • Field Details

    • EDGE_PARSER

      protected static final Function<String,String> EDGE_PARSER
      A function that parses edge labels in the model checker. This identity function is used to convert string representations to and from the model checker's internal format.

    • emptinessOracle

      protected EmptinessOracle.MealyEmptinessOracle<String,String> emptinessOracle
      The oracle used to check for the emptiness of a language, which is essential for disproving properties.

    • modelChecker

      @NotNull protected net.automatalib.modelchecking.ModelChecker.MealyModelChecker<String,String,String,net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>> modelChecker
      The model checker used to verify properties against a Mealy machine, ensuring that the system meets specified Signal Temporal Logic (STL) requirements.

    • inclusionOracle

      protected InclusionOracle.MealyInclusionOracle<String,String> inclusionOracle
      The oracle used to check for the inclusion of one language in another, which is essential for finding counterexamples to hypotheses.

    • memOracle

      protected MembershipOracle.MealyMembershipOracle<String,String> memOracle
      The oracle used to query membership in the language recognized by a Mealy machine, determining whether specific input sequences produce expected outputs.

    • inputAlphabet

      protected net.automatalib.alphabet.Alphabet<String> inputAlphabet
      The alphabet of input symbols used by the Mealy machine, defining the set of valid inputs for the system.

    • STLProperties

      private final List<TemporalLogic<I>> STLProperties
      A list of Signal Temporal Logic (STL) properties that need to be verified against the system.

    • propertyOracles

      private final List<PropertyOracle.MealyPropertyOracle<String,String,String>> propertyOracles
      A list of property oracles used to verify the Signal Temporal Logic (STL) properties against the system.

    • initialized

      boolean initialized
      Flag indicating whether the property oracles have been initialized and are ready for use.

    • reportedFormulas

      private final List<TemporalLogic<I>> reportedFormulas
      A list of Signal Temporal Logic (STL) formulas that have been disproved by the verification process.

    • mapper

      private Optional<Map<String,String>> mapper

  • Constructor Details

    • AbstractAdaptiveSTLUpdater

      public AbstractAdaptiveSTLUpdater()
      Constructs an instance of AbstractAdaptiveSTLUpdater.

      Initializes the model checker used to verify properties against a Mealy machine.

  • Method Details

    • stream

      public Stream<PropertyOracle.MealyPropertyOracle<String,String,String>> stream()
      Returns a stream of property oracles used to verify the Signal Temporal Logic (STL) properties.
      Specified by:
      stream in interface AdaptiveSTLUpdater<I>
      Returns:
      A stream of PropertyOracle.MealyPropertyOracle instances.

    • getPropertyOracles

      public List<PropertyOracle<String,? super net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,?,net.automatalib.word.Word<String>>> getPropertyOracles()
      Returns a list of property oracles used to verify the Signal Temporal Logic (STL) properties.
      Specified by:
      getPropertyOracles in interface BlackBoxOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>
      Returns:
      A list of PropertyOracle.MealyPropertyOracle instances.

    • setMemOracle

      public void setMemOracle(@NotNull MembershipOracle.MealyMembershipOracle<String,String> memOracle)
      Sets the membership oracle and initializes the emptiness and inclusion oracles.
      Specified by:
      setMemOracle in interface AdaptiveSTLUpdater<I>
      Parameters:
      memOracle - The membership oracle to set.

    • addSTLProperty

      protected void addSTLProperty(TemporalLogic<I> stl)
      Adds a Signal Temporal Logic (STL) property to the list of properties to be verified.
      Parameters:
      stl - The STL property to add.

    • addSTLProperties

      protected void addSTLProperties(Collection<? extends TemporalLogic<I>> stlCollection)
      Adds a collection of Signal Temporal Logic (STL) properties to the list of properties to be verified.
      Parameters:
      stlCollection - The collection of STL properties to add.

    • removeSTLProperty

      protected void removeSTLProperty(int index)
      Removes a Signal Temporal Logic (STL) property from the list of properties to be verified.
      Parameters:
      index - The index of the STL property to remove.

    • removeSTLProperties

      protected void removeSTLProperties(Collection<Integer> indices)
      Removes multiple Signal Temporal Logic (STL) properties from the list of properties to be verified.
      Parameters:
      indices - The collection of indices corresponding to the STL properties to remove.

    • confirmInitialization

      private void confirmInitialization()
      Initializes the property oracles if they have not been initialized yet.

      This method is called to set up the inclusion and emptiness oracles, which are necessary for verifying properties. The initialization is delayed until after the membership oracle has been set to ensure proper configuration.

    • newlyFalsifiedFormula

      public final boolean newlyFalsifiedFormula(TemporalLogic<I> stlFormula)
      Checks if a given Signal Temporal Logic (STL) formula has been newly falsified.
      Specified by:
      newlyFalsifiedFormula in interface AdaptiveSTLUpdater<I>
      Parameters:
      stlFormula - The STL formula to check.
      Returns:
      true if the formula has not been previously reported as falsified; otherwise, false.

    • findCounterExample

      @Nullable public @Nullable DefaultQuery<String,net.automatalib.word.Word<String>> findCounterExample(@NotNull @NotNull net.automatalib.automaton.transducer.MealyMachine<?,String,?,String> hypothesis, @NotNull @NotNull Collection<? extends String> inputs)
      Attempts to disprove the current list of STL formulas against the given Mealy machine.

      This method checks each STL formula in the list and tries to find a counterexample that disproves it. It returns:

      • A counterexample for the first newly falsified STL formula, if one exists.
      • A counterexample for the first falsified STL formula, if no new falsifications are found.
      • null, if no counterexamples are found.
      If any formulas are truly disproved, it calls notifyFalsifiedProperty(List) with their indices.
      Specified by:
      findCounterExample in interface EquivalenceOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>
      Parameters:
      hypothesis - The Mealy machine to be verified.
      inputs - The alphabet of the Mealy machine's input symbols.
      Returns:
      A query representing a counterexample if one is found; otherwise, null.
      See Also:

    • notifyFalsifiedProperty

      protected void notifyFalsifiedProperty(List<Integer> falsifiedIndices)
      Notifies that the STL properties at the specified indices are falsified by the currently learned model.

      This method is called when one or more STL properties have been disproved. It allows for generating new adaptive formulas based on these falsifications. Note: The original formulas should not be removed; instead, they can be adapted or extended.

      Parameters:
      falsifiedIndices - A list of indices corresponding to the falsified STL properties.

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • toLTLString

      public String toLTLString(TemporalLogic<I> prop)
      Converts the given Temporal Logic property to its Linear Temporal Logic (LTL) string representation.

      Overrides the default implementation to utilize an optional mapping for abstracting the LTL string.

      Specified by:
      toLTLString in interface AdaptiveSTLUpdater<I>

    • setMapper

      public void setMapper(Map<String,String> mapper)