package ltl
- Alphabetic
- Public
- Protected
Type Members
- sealed abstract class AssertPropertyLike extends AnyRef
The base class for the
AssertProperty
,AssumeProperty
, andCoverProperty
verification constructs.The base class for the
AssertProperty
,AssumeProperty
, andCoverProperty
verification constructs.- Annotations
- @nowarn()
- sealed trait Property extends AnyRef
A Linear Temporal Logic (LTL) property.
- sealed trait Sequence extends Property
A Linear Temporal Logic (LTL) sequence.
- sealed trait SequenceAtom extends AnyRef
A single item that may be used in the
Sequence(...)
convenience constructor for sequences.A single item that may be used in the
Sequence(...)
convenience constructor for sequences. These atoms may either beSequence
s themselves, likea
ora and b
, or aDelayAtom
, likeDelay
. Together they enable a shorthand notation for sequences like:Sequence(a, Delay(), b, Delay(2), c, Delay(3, 9), d, Delay(4, None), e)
.
Value Members
- object AssertProperty extends AssertPropertyLike
Assert that a property holds.
Assert that a property holds.
Use like
AssertProperty(p)
. SeeAssertPropertyLike.apply
for optional clock, disable_iff, and label parameters. - object AssumeProperty extends AssertPropertyLike
Assume that a property holds.
Assume that a property holds.
Use like
AssumeProperty(p)
. SeeAssertPropertyLike.apply
for optional clock, disable_iff, and label parameters. - object CoverProperty extends AssertPropertyLike
Cover that a property holds.
Cover that a property holds.
Use like
CoverProperty(p)
. SeeAssertPropertyLike.apply
for optional clock, disable_iff, and label parameters. - object Delay
The delay atoms available to users.
The delay atoms available to users. Can be interleaved with actual sequences in
Sequence(...)
. SeeSequenceAtom
for details. - object Property
Prefix-style utilities to work with properties.
Prefix-style utilities to work with properties.
This object exposes the primary API to create and compose properties from booleans, sequences, and other properties.
- object Sequence
Prefix-style utilities to work with sequences.
Prefix-style utilities to work with sequences.
This object exposes the primary API to create and compose sequences from booleans and shorter sequences.