| AbstractSliceComplement<S extends SliceVW> |
This class provides a skeleton for the slice-based constructions.
|
| OptimizedSliceComplementOptions |
This class provides the optimized options for the slice-based
complementation.
|
| Slice |
A decorated slice is a pair of ((Q0, b0)(Q1, b1)...(Qn, bn), c) where Qi is a
set of states, bi is in {0, *, 1} indicating whether the corresponding vertex
is guessed to belong to the skeleton (1), is being checked to be a
non-skeleton vertex (0), or is put on hold(*), and c is a boolean indicating
if the last accepting slice has been passed.
|
| SliceAntichain |
This is an implementation of the fixpoint computation described in [Martin De
Wulf, Laurent Doyen, Nicolas Maquet, Jean-François Raskin: Antichains:
Alternative Algorithms for LTL Satisfiability and Model-Checking.
|
| SliceConstruction |
|
| SliceContainment |
Test if an NBW A is contained in another NBW B by constructing the
intersection of A and the complement of B incrementally.
|
| SliceContainmentOptions |
This class contains several options for the slice-based containment.
|
| SliceElement |
A SliceElement is a decorated set of states in a slice.
|
| SliceHelper<S extends SliceVW> |
A SliceHelper is a helper class for the slice-based construction.
|
| SliceKWConstruction |
This class provides an implementation of the slice-based construction [Detlef
Kahler and Thomas Wilke.
|
| SliceKWHelper |
A SliceKWHelper is a helper class for the slice-based construction
[Detlef Kahler and Thomas Wilke.
|
| SliceKWOptions |
This class provides options for the slice-based construction.
|
| SliceOptions |
This class provides options for the slice-based construction.
|
| SliceVW |
A decorated slice is a sequence of pairs (Q0, b0)(Q1, b1)...(Qn, bn) where Qi
is a set of states, bi is in {0, *, 1} indicating whether the corresponding
vertex is guessed to belong to the skeleton (1), is being checked to be a
non-skeleton vertex (0), or is put on hold(*).
|
| SliceVWConstruction |
This class provides an implementation of the preliminary version of the
slice-based construction [Moshe Y.
|
| SliceVWHelper |
A SliceVWHelper is a helper class for the preliminary version of the
slice-based construction [Moshe Y.
|
| SliceVWOptions |
|