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 typeL
- edge label typeAP
- 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 byAbstractDDSolver.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
All Methods Instance Methods Concrete Methods Modifier and Type Method Description Map<L,SolverData<?,T,L,AP>>
getData()
Returns aMap
containing information per procedure name.Map<L,T>
getMayTransformers(TransformerSerializer<T,L,AP> serializer)
Returns aMap
which maps the edge label of may edges to their property transformer.Map<L,T>
getMustTransformers(TransformerSerializer<T,L,AP> serializer)
Returns aMap
which maps the edge label of must edges to their property transformer.List<SolverState<?,T,L,AP>>
getSolverStates()
Returns the list ofSolverState
s, one per update of a node.boolean
isSat()
Returns whether the formula put intoAbstractDDSolver.solveAndRecordHistory(FormulaNode)
is satisfied.
-
-
-
Method Detail
-
getData
public Map<L,SolverData<?,T,L,AP>> getData()
Returns aMap
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 aMap
which maps the edge label of must edges to their property transformer. This method requires aTransformerSerializer
as all property transform are stored asString
s 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 eachSolverState
.
-
getMayTransformers
public Map<L,T> getMayTransformers(TransformerSerializer<T,L,AP> serializer)
Returns aMap
which maps the edge label of may edges to their property transformer. This method requires aTransformerSerializer
as all property transform are stored asString
s 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 eachSolverState
.
-
getSolverStates
public List<SolverState<?,T,L,AP>> getSolverStates()
Returns the list ofSolverState
s, one per update of a node.- Returns:
- the list of
SolverState
s
-
isSat
public boolean isSat()
Returns whether the formula put intoAbstractDDSolver.solveAndRecordHistory(FormulaNode)
is satisfied.- Returns:
true
if formula is satisfied,false
otherwise
-
-