Skip to content

177 subformula traces #178

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
nickovic merged 4 commits into from
Feb 19, 2025
Merged

177 subformula traces #178

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
f32ca30
Addition of the functionality to browse sub-signals + tests.
nickovic Feb 17, 2025
8c2a568
Completed the browsing functionality.
nickovic Feb 19, 2025
44593e7
Tests with python 3.8 only
nickovic Feb 19, 2025
5ac3ddf
Added the description of the get_value() method to README and an exam…
nickovic Feb 19, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ jobs:
runs-on: ubuntu-20.04
strategy:
matrix:
python-version: [3.7, 3.8]
python-version: [3.8]

steps:
- uses: actions/checkout@v1
Expand Down
48 changes: 48 additions & 0 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@
- [Dense-time Offline Monitor](#dense-time-offline-monitor)
- [Discrete-time Specifics](#discrete-time-specifics)
- [Working with time units and timing assumptions](#working-with-time-units-and-timing-assumptions)
- [Features]
- [Accessing evaluation of sub-formulas]
- [References](#references)

<!-- markdown-toc end -->
Expand Down Expand Up @@ -517,6 +519,52 @@ Finally, the following program is correct, because the temporal bound is explici
spec.parse()
...
```
# Features

## Accessing evaluation of sub-formulas

The following example shows how to use the `get_value` method from the
specification object to access the evaluated values of sub-formulas. This works for both
discrete- and dense-time specifications, as well as for online and offline
monitors.

```python
def monitor():
# data
dataset = {
'time': [0, 1, 2],
'a': [100.0, -1.0, -2.0],
'b': [20.0, 2.0, 10.0]
}

# # stl
spec = rtamt.StlDiscreteTimeSpecification()
spec.name = 'HandMadeMonitor'
spec.declare_var('a', 'float')
spec.declare_var('b', 'float')
spec.declare_var('c', 'float')
spec.declare_var('d', 'float')
spec.add_sub_spec('c = a + b')
spec.spec = 'd = c >= - 2'

try:
spec.parse()
except rtamt.RTAMTException as err:
print('RTAMT Exception: {}'.format(err))
sys.exit()

spec.evaluate(dataset)
a = spec.get_value('a')
b = spec.get_value('b')
c = spec.get_value('c')
d = spec.get_value('d')

print('a: ' + str(a))
print('b: ' + str(b))
print('c: ' + str(c))
print('d: ' + str(d))

```

# References

Expand Down
43 changes: 43 additions & 0 deletions examples/features/access_subformulas/access_subformulas.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
#!/usr/bin/env python
import sys
import rtamt

def monitor():
# data
dataset = {
'time': [0, 1, 2],
'a': [100.0, -1.0, -2.0],
'b': [20.0, 2.0, 10.0]
}

# # stl
spec = rtamt.StlDiscreteTimeSpecification()
spec.name = 'HandMadeMonitor'
spec.declare_var('a', 'float')
spec.declare_var('b', 'float')
spec.declare_var('c', 'float')
spec.declare_var('d', 'float')
spec.add_sub_spec('c = a + b')
spec.spec = 'd = c >= - 2'

try:
spec.parse()
except rtamt.RTAMTException as err:
print('RTAMT Exception: {}'.format(err))
sys.exit()

spec.evaluate(dataset)
a = spec.get_value('a')
b = spec.get_value('b')
c = spec.get_value('c')
d = spec.get_value('d')

print('a: ' + str(a))
print('b: ' + str(b))
print('c: ' + str(c))
print('d: ' + str(d))

if __name__ == '__main__':
# Process arguments

monitor()
74 changes: 37 additions & 37 deletions rtamt/explanation/ltl/discrete_time/explainer.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ def __init__(self):
def explain(self, spec):
self.spec = spec
for spec in self.spec.specs:
top_signal = self.spec.offline_results[spec]
top_signal = self.spec.results[spec]
if top_signal[0] < 0:
self.visit(spec, [[[0, 0]], False])

Expand All @@ -23,8 +23,8 @@ def visitConstant(self, element, args):
def visitPredicate(self, element, args):
intervals = args[0]
flag = args[1]
op1_signal = self.spec.offline_results[element.children[0]]
op2_signal = self.spec.offline_results[element.children[1]]
op1_signal = self.spec.results[element.children[0]]
op2_signal = self.spec.results[element.children[1]]
op1_intervals, op2_intervals = explain_predicate(op1_signal, op2_signal, intervals)
self.explanations[element.name] = intervals

Expand All @@ -38,8 +38,8 @@ def visitVariable(self, element, args):
def visitAddition(self, element, args):
intervals = args[0]
flag = args[1]
op1_signal = self.spec.offline_results[element.children[0]]
op2_signal = self.spec.offline_results[element.children[1]]
op1_signal = self.spec.results[element.children[0]]
op2_signal = self.spec.results[element.children[1]]
op1_intervals, op2_intervals = explain_addition(op1_signal, op2_signal, intervals)
self.explanations[element.name] = intervals

Expand All @@ -49,8 +49,8 @@ def visitAddition(self, element, args):
def visitMultiplication(self, element, args):
intervals = args[0]
flag = args[1]
op1_signal = self.spec.offline_results[element.children[0]]
op2_signal = self.spec.offline_results[element.children[1]]
op1_signal = self.spec.results[element.children[0]]
op2_signal = self.spec.results[element.children[1]]
op1_intervals, op2_intervals = explain_multiplication(op1_signal, op2_signal, intervals)
self.explanations[element.name] = intervals

Expand All @@ -60,8 +60,8 @@ def visitMultiplication(self, element, args):
def visitSubtraction(self, element, args):
intervals = args[0]
flag = args[1]
op1_signal = self.spec.offline_results[element.children[0]]
op2_signal = self.spec.offline_results[element.children[1]]
op1_signal = self.spec.results[element.children[0]]
op2_signal = self.spec.results[element.children[1]]
op1_intervals, op2_intervals = explain_subtraction(op1_signal, op2_signal, intervals)
self.explanations[element.name] = intervals

Expand All @@ -71,8 +71,8 @@ def visitSubtraction(self, element, args):
def visitDivision(self, element, args):
intervals = args[0]
flag = args[1]
op1_signal = self.spec.offline_results[element.children[0]]
op2_signal = self.spec.offline_results[element.children[1]]
op1_signal = self.spec.results[element.children[0]]
op2_signal = self.spec.results[element.children[1]]
op1_intervals, op2_intervals = explain_division(op1_signal, op2_signal, intervals)
self.explanations[element.name] = intervals

Expand All @@ -82,7 +82,7 @@ def visitDivision(self, element, args):
def visitAbs(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
op_intervals = explain_abs(op_signal, intervals)
self.explanations[element.name] = intervals

Expand All @@ -91,7 +91,7 @@ def visitAbs(self, element, args):
def visitSqrt(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
op_intervals = explain_sqrt(op_signal, intervals)
self.explanations[element.name] = intervals

Expand All @@ -100,7 +100,7 @@ def visitSqrt(self, element, args):
def visitExp(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
op_intervals = explain_exp(op_signal, intervals)
self.explanations[element.name] = intervals

Expand All @@ -109,8 +109,8 @@ def visitExp(self, element, args):
def visitPow(self, element, args):
intervals = args[0]
flag = args[1]
op1_signal = self.spec.offline_results[element.children[0]]
op2_signal = self.spec.offline_results[element.children[1]]
op1_signal = self.spec.results[element.children[0]]
op2_signal = self.spec.results[element.children[1]]
op1_intervals, op2_intervals = explain_pow(op1_signal, op2_signal, intervals)
self.explanations[element.name] = intervals

Expand All @@ -120,7 +120,7 @@ def visitPow(self, element, args):
def visitRise(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
op_intervals = explain_rise(op_signal, intervals)
self.explanations[element.name] = intervals

Expand All @@ -129,7 +129,7 @@ def visitRise(self, element, args):
def visitFall(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
op_intervals = explain_fall(op_signal, intervals)
self.explanations[element.name] = intervals

Expand All @@ -138,7 +138,7 @@ def visitFall(self, element, args):
def visitNot(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
if flag:
op_intervals = explain_sat_not(op_signal, intervals)
else:
Expand All @@ -150,8 +150,8 @@ def visitNot(self, element, args):
def visitAnd(self, element, args):
intervals = args[0]
flag = args[1]
op1_signal = self.spec.offline_results[element.children[0]]
op2_signal = self.spec.offline_results[element.children[1]]
op1_signal = self.spec.results[element.children[0]]
op2_signal = self.spec.results[element.children[1]]
if flag:
op1_intervals, op2_intervals = explain_sat_and(op1_signal, op2_signal, intervals)
else:
Expand All @@ -164,8 +164,8 @@ def visitAnd(self, element, args):
def visitOr(self, element, args):
intervals = args[0]
flag = args[1]
op1_signal = self.spec.offline_results[element.children[0]]
op2_signal = self.spec.offline_results[element.children[1]]
op1_signal = self.spec.results[element.children[0]]
op2_signal = self.spec.results[element.children[1]]
if flag:
op1_intervals, op2_intervals = explain_sat_or(op1_signal, op2_signal, intervals)
else:
Expand All @@ -178,8 +178,8 @@ def visitOr(self, element, args):
def visitImplies(self, element, args):
intervals = args[0]
flag = args[1]
op1_signal = self.spec.offline_results[element.children[0]]
op2_signal = self.spec.offline_results[element.children[1]]
op1_signal = self.spec.results[element.children[0]]
op2_signal = self.spec.results[element.children[1]]
if flag:
op1_intervals, op2_intervals = explain_sat_implies(op1_signal, op2_signal, intervals)
else:
Expand All @@ -192,8 +192,8 @@ def visitImplies(self, element, args):
def visitIff(self, element, args):
intervals = args[0]
flag = args[1]
op1_signal = self.spec.offline_results[element.children[0]]
op2_signal = self.spec.offline_results[element.children[1]]
op1_signal = self.spec.results[element.children[0]]
op2_signal = self.spec.results[element.children[1]]
if flag:
op1_intervals, op2_intervals = explain_sat_iff(op1_signal, op2_signal, intervals)
else:
Expand All @@ -206,8 +206,8 @@ def visitIff(self, element, args):
def visitXor(self, element, args):
intervals = args[0]
flag = args[1]
op1_signal = self.spec.offline_results[element.children[0]]
op2_signal = self.spec.offline_results[element.children[1]]
op1_signal = self.spec.results[element.children[0]]
op2_signal = self.spec.results[element.children[1]]
if flag:
op1_intervals, op2_intervals = explain_sat_xor(op1_signal, op2_signal, intervals)
else:
Expand All @@ -220,7 +220,7 @@ def visitXor(self, element, args):
def visitEventually(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
if flag:
op_intervals = explain_sat_eventually(op_signal, intervals)
else:
Expand All @@ -232,7 +232,7 @@ def visitEventually(self, element, args):
def visitAlways(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
if flag:
op_intervals = explain_sat_always(op_signal, intervals)
else:
Expand All @@ -248,7 +248,7 @@ def visitUntil(self, element, args):
def visitOnce(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
if flag:
op_intervals = explain_sat_once(op_signal, intervals)
else:
Expand All @@ -260,7 +260,7 @@ def visitOnce(self, element, args):
def visitPrevious(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
if flag:
op_intervals = explain_sat_prev(op_signal, intervals)
else:
Expand All @@ -272,7 +272,7 @@ def visitPrevious(self, element, args):
def visitStrongPrevious(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
if flag:
op_intervals = explain_sat_prev(op_signal, intervals)
else:
Expand All @@ -284,7 +284,7 @@ def visitStrongPrevious(self, element, args):
def visitNext(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
if flag:
op_intervals = explain_sat_next(op_signal, intervals)
else:
Expand All @@ -296,7 +296,7 @@ def visitNext(self, element, args):
def visitStrongNext(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
if flag:
op_intervals = explain_sat_next(op_signal, intervals)
else:
Expand All @@ -308,7 +308,7 @@ def visitStrongNext(self, element, args):
def visitHistorically(self, element, args):
intervals = args[0]
flag = args[1]
op_signal = self.spec.offline_results[element.children[0]]
op_signal = self.spec.results[element.children[0]]
if flag:
op_intervals = explain_sat_historically(op_signal, intervals)
else:
Expand Down
Loading
Loading