Package owl.automaton.algorithm.simulations

Class BuchiSimulation

java.lang.Object

owl.automaton.algorithm.simulations.BuchiSimulation

public final class BuchiSimulation
extends Object

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	BuchiSimulation.SimulationType

Field Summary

Fields

Modifier and Type	Field	Description
static Logger	logger

Constructor Summary

Constructors

Constructor	Description
BuchiSimulation()
BuchiSimulation(ParityGameSolver pgSolver)

Method Summary

Modifier and Type	Method	Description
<S> Set<Pair<S,S>>	backwardSimulation(Automaton<S,? extends BuchiAcceptance> left, Automaton<S,? extends BuchiAcceptance> right, int pebbleCount)
static <S> Automaton<Set<S>,BuchiAcceptance>	compute(Automaton<S,BuchiAcceptance> automaton, AutomatonConversionCommands.NbaSimCommand 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,? extends BuchiAcceptance> left, Automaton<S,? extends BuchiAcceptance> right, int pebbleCount)
<S> Set<Pair<S,S>>	directLookaheadSimulation(Automaton<S,? extends BuchiAcceptance> left, Automaton<S,? extends 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,? extends BuchiAcceptance> left, Automaton<S,? extends BuchiAcceptance> right, int pebbleCount)	Computes the forward multipebble direct simulation for two input automata.
<S> Set<Pair<S,S>>	fairSimulation(Automaton<S,? extends BuchiAcceptance> left, Automaton<S,? extends BuchiAcceptance> right, int pebbleCount)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

logger

public static final Logger logger

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,
                                                                  AutomatonConversionCommands.NbaSimCommand args)

backwardSimulation

public <S> Set<Pair<S,S>> backwardSimulation(Automaton<S,? extends BuchiAcceptance> left,
                                                   Automaton<S,? extends BuchiAcceptance> right,
                                                   int pebbleCount)

fairSimulation

public <S> Set<Pair<S,S>> fairSimulation(Automaton<S,? extends BuchiAcceptance> left,
                                               Automaton<S,? extends BuchiAcceptance> right,
                                               int pebbleCount)

delayedSimulation

public <S> Set<Pair<S,S>> delayedSimulation(Automaton<S,? extends BuchiAcceptance> left,
                                                  Automaton<S,? extends BuchiAcceptance> right,
                                                  int pebbleCount)

directSimulation

public <S> Set<Pair<S,S>> directSimulation(Automaton<S,? extends BuchiAcceptance> left,
                                                 Automaton<S,? extends 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,? extends BuchiAcceptance> left,
                                                          Automaton<S,? extends 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.