public final class Modality extends AbstractSortedOperator
Modifier and Type | Field and Description |
---|---|
static Modality |
BOX
The box operator of dynamic logic.
|
static Modality |
BOX_TRANSACTION
A Java Card transaction version of the box modality.
|
static Modality |
DIA
The diamond operator of dynamic logic.
|
static Modality |
DIA_TRANSACTION
A Java Card transaction version of the diamond modality.
|
private static java.util.Map<java.lang.String,Modality> |
nameMap |
static Modality |
TOUT
The throughout operator of dynamic logic.
|
static Modality |
TOUT_TRANSACTION
A Java Card transaction version of the throughout modality.
|
Modifier | Constructor and Description |
---|---|
private |
Modality(Name name)
creates a modal operator with the given name
|
Modifier and Type | Method and Description |
---|---|
static Modality |
getModality(java.lang.String str)
Returns a modality corresponding to a string
|
boolean |
terminationSensitive()
Whether this modality is termination sensitive,
i.e., it is a "diamond-kind" modality.
|
boolean |
transaction()
Whether this is a transaction modality
|
additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort
arity, bindVarsAt, isRigid, name, toString, validTopLevel, whereToBind
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
arity, bindVarsAt, isRigid, validTopLevel
private static final java.util.Map<java.lang.String,Modality> nameMap
public static final Modality DIA
public static final Modality BOX
public static final Modality DIA_TRANSACTION
public static final Modality BOX_TRANSACTION
public static final Modality TOUT
public static final Modality TOUT_TRANSACTION
private Modality(Name name)
name
- the Name of the modalitypublic static Modality getModality(java.lang.String str)
str
- name of the modality to returnpublic boolean terminationSensitive()
public boolean transaction()