Skip to content

Propositional Formula

masa.common.ltl.Formula

Base class for propositional formulae over atomic proposition labels.

A formula is evaluated against a label set (an iterable of strings), and returns whether the formula is satisfied.

Subclasses must implement sat, which defines the satisfaction relation between the formula and a set of labels.

Notes

The operators provided here are propositional (Boolean) connectives only. Temporal structure is represented externally via a DFA that consumes a trace of label sets.

sat 

sat(labels: Iterable[str]) -> bool

Checks whether the formula is satisfied by the given labels.

Parameters:

Name Type Description Default
labels Iterable[str]

Iterable of atomic proposition names that hold at the current step.

 required

Returns:

Type Description
bool

True if the formula is satisfied under the given labels.

Raises:

Type Description
NotImplementedError

If the subclass does not implement the satisfaction relation.
Source code in masa/common/ltl.py 
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
def sat(self, labels: Iterable[str]) -> bool:
    """Checks whether the formula is satisfied by the given labels.

    Args:
      labels: Iterable of atomic proposition names that hold at the current
        step.

    Returns:
      ``True`` if the formula is satisfied under the given labels.

    Raises:
      NotImplementedError: If the subclass does not implement the
        satisfaction relation.
    """
    raise NotImplementedError(
        "Propositional formula must implement a satisfaction relation"
    )

masa.common.ltl.Atom 

Atom(atom: str)

Bases: Formula

Atomic proposition.

An Atom is satisfied iff the stored atomic proposition name appears in the given label set.

Attributes:

Name Type Description
atom

The atomic proposition name.
Source code in masa/common/ltl.py 
77
78
def __init__(self, atom: str):
    self.atom = atom

atom instance-attribute 

atom = atom

sat 

sat(labels: Iterable[str]) -> bool

Evaluates whether the atom is present in labels.

Parameters:

Name Type Description Default
labels Iterable[str]

Iterable of atomic proposition names.

 required

Returns:

Type Description
bool

True iff atom is in labels.
Source code in masa/common/ltl.py 
80
81
82
83
84
85
86
87
88
89
def sat(self, labels: Iterable[str]) -> bool:
    """Evaluates whether the atom is present in ``labels``.

    Args:
      labels: Iterable of atomic proposition names.

    Returns:
      ``True`` iff :attr:`atom` is in ``labels``.
    """
    return self.atom in labels

masa.common.ltl.Truth 

Truth()

Bases: Formula

Constant truth.

Always satisfied, regardless of the labels.

Source code in masa/common/ltl.py 
98
99
def __init__(self):
    pass

sat 

sat(labels: Iterable[str]) -> bool

Evaluates the truth constant.

Parameters:

Name Type Description Default
labels Iterable[str]

Unused. Included for API consistency.

 required

Returns:

Type Description
bool

True.
Source code in masa/common/ltl.py 
101
102
103
104
105
106
107
108
109
110
def sat(self, labels: Iterable[str]) -> bool:
    """Evaluates the truth constant.

    Args:
      labels: Unused. Included for API consistency.

    Returns:
      ``True``.
    """
    return True

masa.common.ltl.And 

And(subformula_1: Formula, subformula_2: Formula)

Bases: Formula

Conjunction of two subformulae.

Satisfied iff both subformulae are satisfied.

Attributes:

Name Type Description
subformula_1

Left operand.
subformula_2

Right operand.
Source code in masa/common/ltl.py 
123
124
125
def __init__(self, subformula_1: Formula, subformula_2: Formula):
    self.subformula_1 = subformula_1
    self.subformula_2 = subformula_2

subformula_1 instance-attribute 

subformula_1 = subformula_1

subformula_2 instance-attribute 

subformula_2 = subformula_2

sat 

sat(labels: Iterable[str]) -> bool

Evaluates conjunction satisfaction.

Parameters:

Name Type Description Default
labels Iterable[str]

Iterable of atomic proposition names.

 required

Returns:

Type Description
bool

True iff both subformula_1 and subformula_2 are
bool

satisfied by labels.
Source code in masa/common/ltl.py 
127
128
129
130
131
132
133
134
135
136
137
def sat(self, labels: Iterable[str]) -> bool:
    """Evaluates conjunction satisfaction.

    Args:
      labels: Iterable of atomic proposition names.

    Returns:
      ``True`` iff both :attr:`subformula_1` and :attr:`subformula_2` are
      satisfied by ``labels``.
    """
    return self.subformula_1.sat(labels) and self.subformula_2.sat(labels)

masa.common.ltl.Or 

Or(subformula_1: Formula, subformula_2: Formula)

Bases: Formula

Disjunction of two subformulae.

Satisfied iff at least one subformula is satisfied.

Attributes:

Name Type Description
subformula_1

Left operand.
subformula_2

Right operand.
Source code in masa/common/ltl.py 
150
151
152
def __init__(self, subformula_1: Formula, subformula_2: Formula):
    self.subformula_1 = subformula_1
    self.subformula_2 = subformula_2

subformula_1 instance-attribute 

subformula_1 = subformula_1

subformula_2 instance-attribute 

subformula_2 = subformula_2

sat 

sat(labels: Iterable[str]) -> bool

Evaluates disjunction satisfaction.

Parameters:

Name Type Description Default
labels Iterable[str]

Iterable of atomic proposition names.

 required

Returns:

Type Description
bool

True iff either subformula_1 or subformula_2 is
bool

satisfied by labels.
Source code in masa/common/ltl.py 
154
155
156
157
158
159
160
161
162
163
164
def sat(self, labels: Iterable[str]) -> bool:
    """Evaluates disjunction satisfaction.

    Args:
      labels: Iterable of atomic proposition names.

    Returns:
      ``True`` iff either :attr:`subformula_1` or :attr:`subformula_2` is
      satisfied by ``labels``.
    """
    return self.subformula_1.sat(labels) or self.subformula_2.sat(labels)

masa.common.ltl.Neg 

Neg(subformula: Formula)

Bases: Formula

Negation of a subformula.

Satisfied iff the subformula is not satisfied.

Attributes:

Name Type Description
subformula

The formula being negated.
Source code in masa/common/ltl.py 
176
177
def __init__(self, subformula: Formula):
    self.subformula = subformula

subformula instance-attribute 

subformula = subformula

sat 

sat(labels: Iterable[str]) -> bool

Evaluates negation satisfaction.

Parameters:

Name Type Description Default
labels Iterable[str]

Iterable of atomic proposition names.

 required

Returns:

Type Description
bool

True iff subformula is not satisfied by labels.
Source code in masa/common/ltl.py 
179
180
181
182
183
184
185
186
187
188
def sat(self, labels: Iterable[str]) -> bool:
    """Evaluates negation satisfaction.

    Args:
      labels: Iterable of atomic proposition names.

    Returns:
      ``True`` iff :attr:`subformula` is not satisfied by ``labels``.
    """
    return not self.subformula.sat(labels)

masa.common.ltl.Implies 

Implies(subformula_1: Formula, subformula_2: Formula)

Bases: Formula

Implication between two subformulae.

Implies(a, b) is satisfied iff either a is false or b is true under the given labels, i.e. it is equivalent to:

\[ \neg a \lor b \]

Attributes:

Name Type Description
subformula_1

Antecedent (premise).
subformula_2

Consequent (conclusion).
Source code in masa/common/ltl.py 
206
207
208
def __init__(self, subformula_1: Formula, subformula_2: Formula):
    self.subformula_1 = subformula_1
    self.subformula_2 = subformula_2

subformula_1 instance-attribute 

subformula_1 = subformula_1

subformula_2 instance-attribute 

subformula_2 = subformula_2

sat 

sat(labels: Iterable[str]) -> bool

Evaluates implication satisfaction.

Parameters:

Name Type Description Default
labels Iterable[str]

Iterable of atomic proposition names.

 required

Returns:

Type Description
bool

True iff the implication holds under labels.
Source code in masa/common/ltl.py 
210
211
212
213
214
215
216
217
218
219
def sat(self, labels: Iterable[str]) -> bool:
    """Evaluates implication satisfaction.

    Args:
      labels: Iterable of atomic proposition names.

    Returns:
      ``True`` iff the implication holds under ``labels``.
    """
    return Or(Neg(self.subformula_1), self.subformula_2).sat(labels)