Package net.maswag.falcaun

Interface AdaptiveSTLUpdater<I>

Type Parameters:
I - The type of the input at each step.
All Superinterfaces:
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>
All Known Implementing Classes:
AbstractAdaptiveSTLUpdater, AdaptiveSTLList, StaticSTLList, StopDisprovedEQOracle.StaticLTLList
public interface AdaptiveSTLUpdater<I> extends InclusionOracle.MealyInclusionOracle<String,String>, BlackBoxOracle.MealyBlackBoxOracle<String,String>
Interface for a potentially adaptive set of Signal Temporal Logic (STL) formulas. This is primarily for strengthening of STL formulas presented in "Efficient Black-Box Checking via Model Checking with Strengthened Specifications" by Shijubo et al.

This interface defines methods to manage and query a set of STL formulas that can adapt over time based on new information or counterexamples.

It extends both InclusionOracle.MealyInclusionOracle and BlackBoxOracle.MealyBlackBoxOracle.

Author:
Masaki Waga
See Also:

  • Method Details

    • getSTLProperties

      List<TemporalLogic<I>> getSTLProperties()
      Returns the current list of Signal Temporal Logic (STL) formulas.

      The returned list may be updated only after a call to EquivalenceOracle.findCounterExample(A, java.util.Collection<? extends I>).

      Returns:
      A list of STL properties

    • getLTLProperties

      default List<String> getLTLProperties()
      Returns the current list of Linear Temporal Logic (LTL) formulas in their string representations in LTSMin's syntax.
      Returns:
      A list of LTL properties as strings

    • list

      default List<PropertyOracle.MealyPropertyOracle<String,String,String>> list()
      Returns the current list of Linear Temporal Logic (LTL) formulas as PropertyOracle.MealyPropertyOracle instances.
      Returns:
      A list of LTL properties as MealyPropertyOracle instances

    • stream

      Stream<PropertyOracle.MealyPropertyOracle<String,String,String>> stream()
      Returns a stream of Linear Temporal Logic (LTL) formulas as PropertyOracle.MealyPropertyOracle instances.
      Returns:
      A stream of LTL properties as MealyPropertyOracle instances

    • allDisproved

      boolean allDisproved()
      Checks if all the Signal Temporal Logic (STL) properties have been disproved.
      Returns:
      true if all STL properties have been disproved, otherwise false.

    • size

      default int size()
      Returns the number of Signal Temporal Logic (STL) formulas in the current list.
      Returns:
      The number of STL formulas.

    • reset

      void reset()
      Resets the list of Signal Temporal Logic (STL) formulas to their initial state.

    • setMemOracle

      void setMemOracle(@NotNull MembershipOracle.MealyMembershipOracle<String,String> memOracle)
      Sets a new membership oracle.

      This method must be called before invoking list() or stream().

      Parameters:
      memOracle - The new membership oracle to set.

    • setInputAlphabet

      void setInputAlphabet(net.automatalib.alphabet.Alphabet<String> inputAlphabet)
      Sets the input alphabet used for the verification process.
      Parameters:
      inputAlphabet - The input alphabet to set.

    • newlyFalsifiedFormula

      boolean newlyFalsifiedFormula(TemporalLogic<I> stlFormula)
      Checks if a given Signal Temporal Logic (STL) formula has not yet been falsified.
      Parameters:
      stlFormula - The STL formula to check.
      Returns:
      true if the formula has not been falsified, otherwise false.

    • toLTLString

      default String toLTLString(TemporalLogic<I> prop)
      Converts a given Signal Temporal Logic (STL) formula to its Linear Temporal Logic (LTL) string representation.