Example with issues

[havelund]

I think this example has issues:

examples/documentation/time_units_1.py

import sys
import rtamt

def monitor():
spec = rtamt.StlDiscreteTimeSpecification()
spec.name = 'Bounded-response Request-Grant'

spec.declare_var('req', 'float')
spec.declare_var('gnt', 'float')
spec.declare_var('out', 'float')

spec.spec = 'out = (req>=3) implies (eventually[0:5](gnt>=3))'

try:
    spec.parse()
    spec.update(0, [('req', 0.1), ('gnt', 0.3)])
    spec.update(1, [('req', 0.45), ('gnt', 0.12)])
    spec.update(2, [('req', 0.78), ('gnt', 0.18)])
    nb_violations = spec.sampling_violation_counter // nb_violations = 0
except rtamt.RTAMTException as err:
    print('RTAMT Exception: {}'.format(err))
    sys.exit()

if name == 'main':
# Process arguments
monitor()
}

1. ends with }
2. in 'nb_violations = spec.sampling_violation_counter // nb_violations = 0' // should be #
3. it complains about: RTAMT Exception: RTAMT Exception: Bounded eventually operator not implemented in STL online monitor.

[nickovic]

The online monitors can handle only past STL properties. You can pastify bounded future properties by calling `` spec.pastify()after `spec.parse()` . This transforms the bounded future formula phi into an equisatisfiable past formula psi, such that rho(phi, w, t) = rho (psi, w, t + H), where H is the future horizon of the formula phi. Note that now the monitoring verdicts are delayed by H time. So if you want to know the robustness of phi at t, you need to look the output of the monitor for psi at time t+H.

[nickovic]

I realize that this is an example from the repo. In the previous versions of RTAMT, the pastification was done automatically. Now the user must do it explicitly. The example did not change in the meantime. I will update it.

[nickovic]

I double checked the example, and in the master branch it does do spec.pastify() before doing the updates. The example works on my computer. I close this issue.

[havelund]

The example on the website is the following, which still has the problems I mentioned. It seems that the example on the website (README file) is not the same as examples/documentation/time_units_1.py.

examples/documentation/time_units_1.py

import sys
import rtamt

def monitor():
spec = rtamt.StlDiscreteTimeSpecification()
spec.name = 'Bounded-response Request-Grant'

spec.declare_var('req', 'float')
spec.declare_var('gnt', 'float')
spec.declare_var('out', 'float')

spec.spec = 'out = (req>=3) implies (eventually[0:5](gnt>=3))'

try:
    spec.parse()
    spec.update(0, [('req', 0.1), ('gnt', 0.3)])
    spec.update(1, [('req', 0.45), ('gnt', 0.12)])
    spec.update(2, [('req', 0.78), ('gnt', 0.18)])
    nb_violations = spec.sampling_violation_counter // nb_violations = 0
except rtamt.RTAMTException as err:
    print('RTAMT Exception: {}'.format(err))
    sys.exit()

if name == 'main':
# Process arguments
monitor()
}