Package net.automatalib.modelchecker.m3c.solver

Class SolverHistory<T extends AbstractPropertyTransformer<T,L,AP>,L,AP>

java.lang.Object

net.automatalib.modelchecker.m3c.solver.SolverHistory<T,L,AP>

Type Parameters:

T - property transformer type

L - edge label type

AP - atomic proposition type

public final class SolverHistory<T extends AbstractPropertyTransformer<T,L,AP>,L,AP>
extends Object

A class used to store internal information produced by AbstractDDSolver.solveAndRecordHistory(net.automatalib.modelchecker.m3c.formula.FormulaNode<L, AP>) while checking the satisfiability of a formula. The internal information can be used for debugging or visualization purposes.

Method Summary

Modifier and Type	Method	Description
Map<L,SolverData<?,T,L,AP>>	getData()	Returns a Map containing information per procedure name.
Map<L,T>	getMayTransformers(TransformerSerializer<T,L,AP> serializer)	Returns a Map which maps the edge label of may edges to their property transformer.
Map<L,T>	getMustTransformers(TransformerSerializer<T,L,AP> serializer)	Returns a Map which maps the edge label of must edges to their property transformer.
List<SolverState<?,T,L,AP>>	getSolverStates()	Returns the list of SolverStates, one per update of a node.
boolean	isSat()	Returns whether the formula put into AbstractDDSolver.solveAndRecordHistory(FormulaNode) is satisfied.

Methods inherited from class java.lang.Object

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

Method Detail

getData

public Map<L,SolverData<?,T,L,AP>> getData()

Returns a Map containing information per procedure name.

Returns:

a Map containing information per procedure name

getMustTransformers

public Map<L,T> getMustTransformers(TransformerSerializer<T,L,AP> serializer)

Returns a Map which maps the edge label of must edges to their property transformer. This method requires a TransformerSerializer as all property transform are stored as Strings in this class. The returned map is not cached and will be computed on each call. The property transformer of an edge is initialized once and will not be modified which is why this map is only stored once and not in each SolverState.

Parameters:

serializer - used to deserialize each property transformer from a String

Returns:

a Map which maps the edge label of must edges to their property transformer

getMayTransformers

public Map<L,T> getMayTransformers(TransformerSerializer<T,L,AP> serializer)

Returns a Map which maps the edge label of may edges to their property transformer. This method requires a TransformerSerializer as all property transform are stored as Strings in this class. The returned map is not cached and will be computed on each call. The property transformer of an edge is initialized once and will not be modified which is why this map is only stored once and not in each SolverState.

Parameters:

serializer - used to deserialize each property transformer from a String

Returns:

a Map which maps the edge label of may edges to their property transformer

getSolverStates

public List<SolverState<?,T,L,AP>> getSolverStates()

Returns the list of SolverStates, one per update of a node.

Returns:

the list of SolverStates

isSat

public boolean isSat()

Returns whether the formula put into AbstractDDSolver.solveAndRecordHistory(FormulaNode) is satisfied.

Returns:

true if formula is satisfied, false otherwise