Package owl.automaton.symbolic

Class DFISymbolicDPASolver

java.lang.Object

owl.automaton.symbolic.DFISymbolicDPASolver

All Implemented Interfaces:

SymbolicDPASolver

public class DFISymbolicDPASolver
extends Object
implements SymbolicDPASolver

This is a symbolic implementation of the explicit fix-point iteration algorithm with freezing as described in https://doi.org/10.4204/EPTCS.305.9. The symbolic implementation is based on http://essay.utwente.nl/81974/ but is adapted to operate on the automaton directly instead of converting to a game first.

Nested Class Summary

Nested classes/interfaces inherited from interface owl.automaton.symbolic.SymbolicDPASolver

SymbolicDPASolver.Solution

Constructor Summary

Constructors

Constructor	Description
DFISymbolicDPASolver()

Method Summary

Modifier and Type	Method	Description
SymbolicDPASolver.Solution	solve(SymbolicAutomaton<? extends ParityAcceptance> dpa, ImmutableBitSet controlledAps)

Methods inherited from class java.lang.Object

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

Constructor Detail

DFISymbolicDPASolver

public DFISymbolicDPASolver()

Method Detail

solve

public SymbolicDPASolver.Solution solve(SymbolicAutomaton<? extends ParityAcceptance> dpa,
                                        ImmutableBitSet controlledAps)

Specified by:

solve in interface SymbolicDPASolver