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 Map<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(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
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(String str)
str
- name of the modality to returnpublic boolean terminationSensitive()
public boolean transaction()