Package org.svvrl.goal.core.comp.safra

Class SafraConstruction

java.lang.Object

org.svvrl.goal.core.AbstractAlgorithm

org.svvrl.goal.core.AbstractControllableAlgorithm

org.svvrl.goal.core.AbstractEditableAlgorithm

org.svvrl.goal.core.comp.AbstractComplementConstruction<FSA,FSA>

org.svvrl.goal.core.comp.safra.SafraConstruction

All Implemented Interfaces:

java.util.EventListener, Algorithm, AlgorithmListener, ComplementConstruction<FSA,FSA>, ControllableAlgorithm, EditableAlgorithm

Direct Known Subclasses:

ModifiedSafraConstruction

public class SafraConstruction
extends AbstractComplementConstruction<FSA,FSA>

A SafraComplement object complements an NBW A in stages:

1. Determinizes the input NBW A as a DRW R by the Safra's construction.
2. Complements R as a DSW S by interpreting the acceptance condition of R as a Streett condition.
3. Converts S to an NBW A'.

This class also offers a modified version of Safra's construction. See SafraConverter for more details.

Author:

Ming-Hsien Tsai

Field Summary

Fields

Modifier and Type	Field	Description
static java.lang.String	O_ACCEPTING_TRUE_LOOPS	The option of simplifying accepting true loops.
static java.lang.String	O_ALL_SUCCESSORS_ACCEPTING	The option of simplification when all successors are accepting.
static java.lang.String	O_HISTORY_TREE	The option of using Schewe's history trees instead of Safra trees.

Constructor Summary

Constructors

Modifier	Constructor	Description
	SafraConstruction(FSA aut)	Constructs this object with an NBW to be complemented.
protected	SafraConstruction(FSA aut, boolean m)	Constructs this object with an NBW to be complemented and a boolean indicating if the modified version should be used.
	SafraConstruction(FSA aut, Properties options)	Constructs this object with an NBW to be complemented and custom options for Safra's construction.
protected	SafraConstruction(FSA aut, Properties opt, boolean m)	Constructs this object with an NBW to be complemented, custom options for Safra's construction, a boolean indicating if the modified version should be used.

Method Summary

Modifier and Type	Method	Description
FSA	complement()	Performs the complementation and returns the complement.
FSA	getIntermediateResult()	Returns the intermediate result.

Methods inherited from class org.svvrl.goal.core.comp.AbstractComplementConstruction

getInput

Methods inherited from class org.svvrl.goal.core.AbstractControllableAlgorithm

addControllableListener, addSubAlgorithm, doPause, doStage, doStart, doStep, fireReferenceChangedEvent, getInterval, getStages, getStatus, pause, pause, removeControllableListener, removeSubAlgorithm, setInterval, setStages, setStatus, setSynchronizationObject, stagePause, stagePause

Methods inherited from class org.svvrl.goal.core.AbstractAlgorithm

addAlgorithmListener, addProgress, appendStageMessage, appendStepMessage, getAlgorithmListeners, getCurrentProgress, getMaximalProgress, getMinimalProgress, getName, getOptions, getSubAlgorithms, isDeterministicProgress, removeAlgorithmListener, setCurrentProgress, setDeterministicProgress, setMaximalProgress, setMinimalProgress

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.svvrl.goal.core.Algorithm

addAlgorithmListener, getAlgorithmListeners, getOptions, removeAlgorithmListener

Methods inherited from interface org.svvrl.goal.core.AlgorithmListener

appendStageMessage, appendStepMessage, getCurrentProgress, getMaximalProgress, getMinimalProgress, setCurrentProgress, setDeterministicProgress, setMaximalProgress, setMinimalProgress

Methods inherited from interface org.svvrl.goal.core.ControllableAlgorithm

addControllableListener, doPause, doStage, doStart, doStep, getInterval, getStages, getStatus, removeControllableListener, setInterval, setStages, setStatus, setSynchronizationObject

Field Details

O_HISTORY_TREE

public static final java.lang.String O_HISTORY_TREE

The option of using Schewe's history trees instead of Safra trees.

O_ACCEPTING_TRUE_LOOPS

public static final java.lang.String O_ACCEPTING_TRUE_LOOPS

The option of simplifying accepting true loops.

O_ALL_SUCCESSORS_ACCEPTING

public static final java.lang.String O_ALL_SUCCESSORS_ACCEPTING

The option of simplification when all successors are accepting.

Constructor Details

SafraConstruction

public SafraConstruction(FSA aut)

Constructs this object with an NBW to be complemented. The default options for Safra's construction will be used.

Parameters:

aut - an NBW to be complemented

Throws:

java.lang.IllegalArgumentException - if aut is not an NBW

SafraConstruction

public SafraConstruction(FSA aut, Properties options)

Constructs this object with an NBW to be complemented and custom options for Safra's construction.

Parameters:

aut - an NBW to be complemented

options - custom options for Safra's construction

Throws:

java.lang.IllegalArgumentException - if aut is not an NBW

SafraConstruction

protected SafraConstruction(FSA aut, boolean m)

Constructs this object with an NBW to be complemented and a boolean indicating if the modified version should be used. The default options for Safra's construction will be used.

Parameters:

aut - an NBW to be complemented

m - a boolean indicating if the modified version should be used

Throws:

java.lang.IllegalArgumentException - if aut is not an NBW

SafraConstruction

protected SafraConstruction(FSA aut, Properties opt, boolean m)

Constructs this object with an NBW to be complemented, custom options for Safra's construction, a boolean indicating if the modified version should be used.

Parameters:

aut - an NBW to be complemented

opt - custom options for Safra's construction

m - a boolean indicating if the modified version should be used

Throws:

java.lang.IllegalArgumentException - if aut is not an NBW

Method Details

getIntermediateResult

public FSA getIntermediateResult()

Description copied from interface: EditableAlgorithm

Returns the intermediate result.

Returns:

the intermediate result of this algorithm

complement

public FSA complement()

Description copied from interface: ComplementConstruction

Performs the complementation and returns the complement.

Returns:

the complement of the input automaton returned by ComplementConstruction.getInput()