package mcrl2
- Alphabetic
- Public
- All
Type Members
-
class
FreshNames[A] extends AnyRef
A map-like class generating fresh values for keys of type A.
A map-like class generating fresh values for keys of type A.
The first time an unknown key is accessed, a fresh identifier is created (of type
String, using the givenprefixandsuffix); the identifier is remembered, and returned for future calls.- Attributes
- protected
-
case class
Proc(current: List[String] = List(), defs: List[String] = List()) extends Product with Serializable
An mCRL2 process, constructed by the encoding procedure.
An mCRL2 process, constructed by the encoding procedure.
A process consists of a
currentpart (being built by the encoder), and a series of process definitions (defs). The two will be later merged in a single string, and then in a single.mcrl2file- Attributes
- protected
-
abstract
class
Property extends AnyRef
A property, i.e., an mCRL2 formula to verify mpstk.mcrl2.Specs.
A property, i.e., an mCRL2 formula to verify mpstk.mcrl2.Specs.
- Attributes
- protected[mpstk]
-
class
Spec extends AnyRef
A mCRL2 specification, obtained from a typing context.
-
class
Verifier extends LazyLogging
Playground to verify whether a set of mpstk.mcrl2.Specs satisfy a set of mpstk.mcrl2.Property.
Playground to verify whether a set of mpstk.mcrl2.Specs satisfy a set of mpstk.mcrl2.Property.
- Attributes
- protected[mpstk]
Value Members
-
object
DeadlockFreedom extends Property with Product with Serializable
Deadlock freedom property.
- object FreshNames
-
object
Liveness extends Property with Product with Serializable
Liveness property.
-
object
LivenessPlus extends Property with Product with Serializable
Liveness+ property.
-
object
LivenessPlusPlus extends Property with Product with Serializable
Liveness+ property.
-
object
NeverTermination extends Property with Product with Serializable
Never-termination property.
-
object
Properties
A container for the properties available on mpstk.
-
object
Safety extends Property with Product with Serializable
Safety property.
- object Spec
-
object
Termination extends Property with Product with Serializable
Termination property.
- object Verifier