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:
de.learnlib.oracle.BlackBoxOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, de.learnlib.oracle.BlackBoxOracle.MealyBlackBoxOracle<String,String>, de.learnlib.oracle.EquivalenceOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, de.learnlib.oracle.EquivalenceOracle.MealyEquivalenceOracle<String,String>, de.learnlib.oracle.InclusionOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>, de.learnlib.oracle.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 for potentially adaptive set of STL formulas
Author:
Masaki Waga
See Also:

  • Field Details

    • EDGE_PARSER

      protected static final Function<String,String> EDGE_PARSER

    • emptinessOracle

      protected de.learnlib.oracle.EmptinessOracle.MealyEmptinessOracle<String,String> emptinessOracle

    • modelChecker

      @NotNull protected net.automatalib.modelchecking.ModelChecker.MealyModelChecker<String,String,String,net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>> modelChecker

    • inclusionOracle

      protected de.learnlib.oracle.InclusionOracle.MealyInclusionOracle<String,String> inclusionOracle

    • memOracle

      protected de.learnlib.oracle.MembershipOracle.MealyMembershipOracle<String,String> memOracle

    • inputAlphabet

      protected net.automatalib.alphabet.Alphabet<String> inputAlphabet

    • STLProperties

      private final List<TemporalLogic<I>> STLProperties

    • propertyOracles

      private final List<de.learnlib.oracle.PropertyOracle.MealyPropertyOracle<String,String,String>> propertyOracles

    • initialized

      boolean initialized

    • reportedFormulas

      private final List<TemporalLogic<I>> reportedFormulas

  • Constructor Details

    • AbstractAdaptiveSTLUpdater

      public AbstractAdaptiveSTLUpdater()

  • Method Details

    • stream

      public Stream<de.learnlib.oracle.PropertyOracle.MealyPropertyOracle<String,String,String>> stream()
      Description copied from interface: AdaptiveSTLUpdater
      Returns the current list of LTL formulas in MealyPropertyOracle in stream
      Specified by:
      stream in interface AdaptiveSTLUpdater<I>

    • getPropertyOracles

      public List<de.learnlib.oracle.PropertyOracle<String,? super net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,?,net.automatalib.word.Word<String>>> getPropertyOracles()
      Specified by:
      getPropertyOracles in interface de.learnlib.oracle.BlackBoxOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>

    • setMemOracle

      public void setMemOracle(@NotNull de.learnlib.oracle.MembershipOracle.MealyMembershipOracle<String,String> memOracle)
      Description copied from interface: AdaptiveSTLUpdater
      Set new membership oracle. This is necessary to call list() and stream()
      Specified by:
      setMemOracle in interface AdaptiveSTLUpdater<I>

    • addSTLProperty

      protected void addSTLProperty(TemporalLogic<I> stl)

    • addSTLProperties

      protected void addSTLProperties(Collection<? extends TemporalLogic<I>> stlCollection)

    • removeSTLProperty

      protected void removeSTLProperty(int index)

    • removeSTLProperties

      protected void removeSTLProperties(Collection<Integer> indices)

    • confirmInitialization

      private void confirmInitialization()
      Initialize property oracles if they are not initialized yet.

      We do not initialize it in the constructor to delay the construction of the membership oracle.

    • newlyFalsifiedFormula

      public final boolean newlyFalsifiedFormula(TemporalLogic<I> stlFormula)
      Description copied from interface: AdaptiveSTLUpdater
      Returns if the formula is not yet falsified
      Specified by:
      newlyFalsifiedFormula in interface AdaptiveSTLUpdater<I>

    • findCounterExample

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

      It returns

      • a counterexample for the newly falsified STL formula, if exists
      • a counterexample for the first falsified STL formula, if exists
      • null, if no counterexample is found.
      We call notifyFalsifiedProperty with the indices of the truly falsified formulas.
      Specified by:
      findCounterExample in interface de.learnlib.oracle.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.
      Returns:
      A query of counterexample if a counterexample is found. Otherwise, it returns null.
      See Also:
      • CExFirstOracle

    • notifyFalsifiedProperty

      protected void notifyFalsifiedProperty(List<Integer> falsifiedIndices)
      Notify that this.getLTLProperties.get(i) is falsified by the currently learned model.

      Typically, we can generate a new adaptive formula. Note: we should not remove the original formula by this.

      Parameters:
      falsifiedIndices - The set of indices of the falsified LTL formulas

    • toString

      public String toString()
      Overrides:
      toString in class Object