rwth.i2.ltlrv.management
Class Configuration

java.lang.Object
  rwth.i2.ltlrv.management.Configuration

public class Configuration
extends Object

Configuration - Global configuration for one single formula.

Author:

Eric Bodden

Field Summary

private Set<Set<IAFAState>>	globalState The current global state as a disjunct of conjuncts of terms.
private static int	lastTermNumber Last number a term was mapped to.
private static Map<IAFAState,Integer>	termToNumber Maps a term to a number.

Constructor Summary

Configuration(IAFAState initialState)
Constructs a new configuration for an initial state.

Method Summary

private static String	clauseSetToString(Set<Set<IAFAState>> clauseSet)
boolean	equals(Object oth)
private static WeakValuesMap<String,Object>	filterBindingForCurrentJoinpoint(WeakValuesMap<String,Object> binding, Collection<String> unboundVariablesAtCurrentJoinpoint) Filters a binding for those entries that are unbound at the current joinpoint.
int	hashCode()
private static boolean	isClauseSetFinal(Set<Set<IAFAState>> clauseSet)
boolean	isFF() Returns true if this configuration is in the global state FF.
boolean	isFinal() Returns true if this configuration is currently in a final (accepting) state.
boolean	isTT() Returns true if this configuration is in the global state TT.
private static int	numberOf(IAFAState term) Returns a (possibly new) number for a term, based on equality.
private static String	numberStringOf(IAFAState term) Returns a unique number string for the term, based on equality.
private static Set<Set<IAFAState>>	subsumptionReduction(Set<Set<IAFAState>> set) Removes sets which contain another set (in order to find the smallest model)
String	toString()
(package private) void	transition(PropositionSet props) Performs a transition for the given propositions.
private static Set<Set<IAFAState>>	transition(Set<Set<IAFAState>> globalState, PropositionSet currentProps) Performs a transition from the given state (set of clauses) to the sucessor state for the given set of propositions.

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

globalState

private Set<Set<IAFAState>> globalState

The current global state as a disjunct of conjuncts of terms.

termToNumber

private static Map<IAFAState,Integer> termToNumber

Maps a term to a number. For debugging purposes only.

lastTermNumber

private static int lastTermNumber

Last number a term was mapped to. For debugging purposes only.

Constructor Detail

Configuration

public Configuration(IAFAState initialState)
              throws IAFAState.ValidationException

Constructs a new configuration for an initial state.

Parameters:

initialState - the initial state of the system

Throws:

IAFAState.ValidationException - thrown if there are inconsistent bindings in this formula

Method Detail

transition

void transition(PropositionSet props)

Performs a transition for the given propositions.

Parameters:

props - a set of runtime propositions

isFinal

public boolean isFinal()

Returns true if this configuration is currently in a final (accepting) state.

Returns:

true iff the configuration is final/accepting

isClauseSetFinal

private static boolean isClauseSetFinal(Set<Set<IAFAState>> clauseSet)

Parameters:

clauseSet - the clause set to check

Returns:

true is this clause set represents a final state

isTT

public boolean isTT()

Returns true if this configuration is in the global state TT.

Returns:

true if the global state of this configuration is {{}}

isFF

public boolean isFF()

Returns true if this configuration is in the global state FF.

Returns:

true if the global state of this configuration is {}

transition

private static Set<Set<IAFAState>> transition(Set<Set<IAFAState>> globalState,
                                              PropositionSet currentProps)

Performs a transition from the given state (set of clauses) to the sucessor state for the given set of propositions.

Parameters:

globalState - the state to calculate the successor for

currentProps - the set of propositions to calculate the transition for

Returns:

the new state (set of clauses)

filterBindingForCurrentJoinpoint

private static WeakValuesMap<String,Object> filterBindingForCurrentJoinpoint(WeakValuesMap<String,Object> binding,
                                                                             Collection<String> unboundVariablesAtCurrentJoinpoint)

Filters a binding for those entries that are unbound at the current joinpoint.

Parameters:

binding - A full binding at the current joinpoint.

unboundVariablesAtCurrentJoinpoint - collection of variabels that are unbound at the current joinpoint in the given formula

Returns:

the filtered map of bindings

subsumptionReduction

private static Set<Set<IAFAState>> subsumptionReduction(Set<Set<IAFAState>> set)

Removes sets which contain another set (in order to find the smallest model)

Parameters:

set - the set on which the reduction should be performed

Returns:

the redueced set

toString

public String toString()

Overrides:

toString in class Object

clauseSetToString

private static String clauseSetToString(Set<Set<IAFAState>> clauseSet)

Parameters:

clauseSet - set to return a string for

Returns:

a string representation of the clause set

numberOf

private static int numberOf(IAFAState term)

Returns a (possibly new) number for a term, based on equality.

Parameters:

term - a term

Returns:

a (possibly new) unique number for this term

numberStringOf

private static String numberStringOf(IAFAState term)

Returns a unique number string for the term, based on equality.

Parameters:

term - a term

Returns:

a unique number string for this term

equals

public boolean equals(Object oth)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object