Class BuchiSimulation
- java.lang.Object
-
- owl.automaton.algorithm.simulations.BuchiSimulation
-
public final class BuchiSimulation extends Object
-
-
Field Summary
Fields Modifier and Type Field Description static OwlModule<OwlModule.Transformer>
MODULE
-
Constructor Summary
Constructors Constructor Description BuchiSimulation()
BuchiSimulation(ParityGameSolver pgSolver)
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description <S> Set<Pair<S,S>>
backwardSimulation(Automaton<S,BuchiAcceptance> left, Automaton<S,BuchiAcceptance> right, int pebbleCount)
static <S> Automaton<Set<S>,BuchiAcceptance>
compute(Automaton<S,BuchiAcceptance> automaton, BuchiSimulationArguments args)
static <S> Set<Pair<S,S>>
computeEquivalence(Set<Pair<S,S>> relation)
Computes an equivalence relation based on a given preorder.<S> Set<Pair<S,S>>
delayedSimulation(Automaton<S,BuchiAcceptance> left, Automaton<S,BuchiAcceptance> right, int pebbleCount)
<S> Set<Pair<S,S>>
directLookaheadSimulation(Automaton<S,BuchiAcceptance> left, Automaton<S,BuchiAcceptance> right, int maxLookahead)
<S> boolean
directSimulates(Automaton<S,BuchiAcceptance> left, Automaton<S,BuchiAcceptance> right, S leftState, S rightState, int pebbleCount)
Checks if two states are forward-direct multipebble similar.<S> Set<Pair<S,S>>
directSimulation(Automaton<S,BuchiAcceptance> left, Automaton<S,BuchiAcceptance> right, int pebbleCount)
Computes the forward multipebble direct simulation for two input automata.<S> Set<Pair<S,S>>
fairSimulation(Automaton<S,BuchiAcceptance> left, Automaton<S,BuchiAcceptance> right, int pebbleCount)
static void
main(String... args)
Entry point for the execution of 'nbasim' start script.
-
-
-
Field Detail
-
MODULE
public static final OwlModule<OwlModule.Transformer> MODULE
-
-
Constructor Detail
-
BuchiSimulation
public BuchiSimulation()
-
BuchiSimulation
public BuchiSimulation(ParityGameSolver pgSolver)
-
-
Method Detail
-
computeEquivalence
public static <S> Set<Pair<S,S>> computeEquivalence(Set<Pair<S,S>> relation)
Computes an equivalence relation based on a given preorder.- Type Parameters:
S
- The elements put in relation by the preorder- Parameters:
relation
- The input preorder relation- Returns:
- The equivalence relation induced by the input preorder
-
compute
public static <S> Automaton<Set<S>,BuchiAcceptance> compute(Automaton<S,BuchiAcceptance> automaton, BuchiSimulationArguments args)
-
main
public static void main(String... args) throws IOException
Entry point for the execution of 'nbasim' start script.- Throws:
IOException
-
backwardSimulation
public <S> Set<Pair<S,S>> backwardSimulation(Automaton<S,BuchiAcceptance> left, Automaton<S,BuchiAcceptance> right, int pebbleCount)
-
fairSimulation
public <S> Set<Pair<S,S>> fairSimulation(Automaton<S,BuchiAcceptance> left, Automaton<S,BuchiAcceptance> right, int pebbleCount)
-
delayedSimulation
public <S> Set<Pair<S,S>> delayedSimulation(Automaton<S,BuchiAcceptance> left, Automaton<S,BuchiAcceptance> right, int pebbleCount)
-
directSimulation
public <S> Set<Pair<S,S>> directSimulation(Automaton<S,BuchiAcceptance> left, Automaton<S,BuchiAcceptance> right, int pebbleCount)
Computes the forward multipebble direct simulation for two input automata. Spoiler moves within the left and Duplicator within the right automaton. For autosimulation left and right automaton should just coincide.- Type Parameters:
S
- The type of state for both input automata.- Parameters:
left
- Input automaton Spoiler moves in.right
- Duplicator's arena automaton.pebbleCount
- The maximum number of pebbles Duplicator can control.- Returns:
- A set of forward multipebble similar states.
-
directLookaheadSimulation
public <S> Set<Pair<S,S>> directLookaheadSimulation(Automaton<S,BuchiAcceptance> left, Automaton<S,BuchiAcceptance> right, int maxLookahead)
-
directSimulates
public <S> boolean directSimulates(Automaton<S,BuchiAcceptance> left, Automaton<S,BuchiAcceptance> right, S leftState, S rightState, int pebbleCount)
Checks if two states are forward-direct multipebble similar.- Type Parameters:
S
- Type of state of the two input automata.- Parameters:
left
- Spoiler automaton.right
- Duplicator automaton.leftState
- Spoiler starting state.rightState
- Duplicator starting state.pebbleCount
- Number of pebble Duplicator can control at most.- Returns:
- true if and only if leftState is simulated by rightState.
-
-