Package eu.iv4xr.framework.extensions.ltl

Class Buchi

java.lang.Object
eu.iv4xr.framework.extensions.ltl.Buchi
public class Buchi extends Object
Represent a Buchi automaton. An "execution" of such an automaton is a path through the automaton, starting with its initial state. Only a single initial state is allowed. A Buchi automaton defines acceptance over infinite executions. So, it decides if a given infinite execution is accepted or else rejected. As such, a Buchi automaton can be seen as representing some predicate over infinite executions.

In the context of 'model checking' a Buchi automaton is used to check if another program (called 'environment') can produce an execution that would be accepted by the Buchi. To check this, the Buchi would the be executed 'together' with the environment. A transition in the Buchi is only possible if the transition relation of the Buchi itself allows this, and if furthermore the current state of the environment satisfies the guarding condition of the Buchi.

Obviously checking an infinite sequence by literally iterating over it is not possible. So a Buchi automaton decides acceptance based on a finite segment that we will call witness. An infinite sequence is 'accepted' if it can be obtained by 'extending' a witness. There are two concepts of 'extending', explained below.

Formally we define a Buchi automaton as a structure B = (s0,S,R,O,F) where S is a finite set of states, s0 is the automaton initial state. R is some function describing the transitions in the automaton. A transition connect an state s to some destination state t in S. But a transition is also labeled by a state-predicate p, which is meant to be evaluated on the state of the 'environment' mentioned before. When the Buchi is executed together with this environment, a transition in the Buchi can only be taken if its condition p evaluates to true when evaluated on the state of this environment.

O and F are subsets of S defining acceptance, where O defines Buchi's usual omega-acceptance, and F defines non-omega acceptance. The F-component deviates from the standard definition of Buchi. It is also not necessary as F-acceptance can also be expressed using O-acceptance. However, the F-component makes modeling with a Buchi a bit more intuitive.

Acceptance is defined as follows:

  • A finite execution sigma that ends in a state in F is a witness. Any infinite execution tau, of which sigma is a prefix, is considered as accepted by the Buchi automaton.
  • A finite execution sigma of the form s0++[o]++s1++[o], where s0 is some prefix, s1 is some middle part, and o is a state in O, is a witness. Notice that such a sigma contains thus a cycle that passes o. Any infinite execution tau, that can be obtained from sigma by repeating its o-cycle is considered as accepted by the Buchi automaton.
Author:
Wish

  • Field Details

    • states

      Map<String,​Integer> states
      Contain all states-names, along to their mapping to integer indices as their assigned ids. Model check will operate on those ids instead of names.

    • decoder

      String[] decoder
      decoder[i] gives the name of the state with assigned-id i.

    • initialState

      public int initialState

    • currentState

      public int currentState

    • omegaAcceptingStates

      public Set<Integer> omegaAcceptingStates

    • traditionalAcceptingStates

      public Set<Integer> traditionalAcceptingStates

    • transitions

      public Map<Integer,​List<Pair<Buchi.BuchiTransition,​Integer>>> transitions

    • currentExecution

      public List<Integer> currentExecution
      When 'executing' this Buchi (transitioning from one state to another) this list io used to keep track the execution so far (the sequence of states of the Buchi that is passed by the execution).

  • Constructor Details

    • Buchi

      public Buchi()

  • Method Details

    • withStates

      public Buchi withStates​(String... stateNames)
      Set the states of this Buchi to the given states. The method then returns this Buchi.

    • withTransition

      public Buchi withTransition​(String from, String to, String transitionId, String transitionName, Predicate<IExplorableState> condition)
      Add the given transition to this Buchi. The method then returns this Buchi.
      Parameters:
      from - The source-state of the transition.
      to - The destination-state of the transition.
      transitionId - Some id to identify the transition.
      transitionName - The name of the transition. It does not have to be unique.
      condition - The semantic condition specifying when the transition can be taken.

    • withTransition

      public Buchi withTransition​(String from, String to, String transitionId, Predicate<IExplorableState> condition)
      The same as the other withTransition. This one will set the transition name to be the same as the given transitionId.

    • withInitialState

      public Buchi withInitialState​(String sinit)
      Set the initial state of this Buchi. The method then returns this Buchi.

    • withOmegaAcceptance

      public Buchi withOmegaAcceptance​(String... Ostates)
      Set the set of omega-accepting states. The method then returns this Buchi.

    • withNonOmegaAcceptance

      public Buchi withNonOmegaAcceptance​(String... NonOstates)
      Set the set of non-omega-accepting states. The method then returns this Buchi.

    • reset

      public void reset()
      Reset this Buchi to its initial state.

    • transitionTo

      public void transitionTo​(int newBuchiState)
      Execute a transition to a new state. In favor for speed, this method won't check if the transition is actually possible on the current state. The caller is responsible for checking this prior to calling this method.

    • numberOfTransitions

      public int numberOfTransitions()
      Just returning the total number of transitions that this Buchi has.

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • treeClone

      public Buchi treeClone()
      Construct a new Buchi that is a "clone" of this Buchi. he states and transitions will be cloned, but the underlying predicates that form the transitions' conditions are not cloned.

    • appendStateNames

      Buchi appendStateNames​(String suffix)
      Rename the states in this Buchi, by adding the given string as a suffix to each state-name. It then returns the resulting Buchi.

    • insertNewState

      Buchi insertNewState​(String st)
      Insert a new state with the given name. The new state will get the index 0. The indices of existing states will be shifted by 1, and their arrows will be adjusted accordingly. The method return the modified Buchi.

    • backtrackToPreviousState

      public void backtrackToPreviousState()
      Cause this Buchi to backtrack to the previous state in the current execution.

    • getEnabledTransitions

      public List<Pair<Buchi.BuchiTransition,​Integer>> getEnabledTransitions​(IExplorableState state)
      Check which of transitions of this Buchi, that go from from it current state, would be semantically possible/enabled given the concrete state of the environment with which this Buchi is executed.