Package net.maswag.falcaun

Class StopDisprovedEQOracle.StaticLTLList<I>

java.lang.Object
net.maswag.falcaun.AbstractAdaptiveSTLUpdater<I>
net.maswag.falcaun.StopDisprovedEQOracle.StaticLTLList<I>
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>
Enclosing class:
StopDisprovedEQOracle<I,O,C>
static class StopDisprovedEQOracle.StaticLTLList<I> extends AbstractAdaptiveSTLUpdater<I>

  • Field Details

  • Constructor Details

    • StaticLTLList

      StaticLTLList(List<String> ltlProperties)

  • Method Details

    • getLTLProperties

      public List<String> getLTLProperties()
      Description copied from interface: AdaptiveSTLUpdater
      Returns the current list of LTL formulas in the string representation

    • size

      public int size()
      Description copied from interface: AdaptiveSTLUpdater
      Returns the number of the current list of STL formulas

    • 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>
      Overrides:
      stream in class AbstractAdaptiveSTLUpdater<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)
      Find a counter example using the current list of STL formulas
      Specified by:
      findCounterExample in interface de.learnlib.oracle.EquivalenceOracle<net.automatalib.automaton.transducer.MealyMachine<?,String,?,String>,String,net.automatalib.word.Word<String>>
      Overrides:
      findCounterExample in class AbstractAdaptiveSTLUpdater<I>
      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:
      • ::findCounterExample

    • notifyFalsifiedProperty

      protected void notifyFalsifiedProperty(List<Integer> falsifiedIndices)
      Description copied from class: AbstractAdaptiveSTLUpdater
      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.

      Overrides:
      notifyFalsifiedProperty in class AbstractAdaptiveSTLUpdater<I>
      Parameters:
      falsifiedIndices - The set of indices of the falsified LTL formulas

    • allDisproved

      public boolean allDisproved()
      Description copied from interface: AdaptiveSTLUpdater
      Returns if all the properties are disproved

    • reset

      public void reset()
      Description copied from interface: AdaptiveSTLUpdater
      Reset the list of the STL formulas to the initial one.