Model Checking

Model Assertions

Moddy 1.5 added a possibility for checkers in the model to tell the simulator that it detected some abnormal situation, e.g. encountered an invalid state, a result is out of range or some timeout has occurred.

A moddy part can call the following method to signal a problem (An example can be found in 6_vthread_remote_controlled.py):

self.assertion_failed('3rd invocation assertion')

By default, such an assertion failure causes the simulation to stop, unless you pass stop_on_assertion_failure=False to the simulators run() method. In this case, the simulator gathers all assertions during the simulation and prints a summary at the end of the simulation:

1 Assertion failures during simulation
    260.0s 3rd invocation assertion: in run_vthread, (6_vthread_remote_controlled.py::37)

Assertion failures are also displayed in the sequence diagram in purple color:

Model Monitors

Moddy 1.10 added a possibility to register functions that gets called at each simulation step. More specifically, they are called at the end of each simulation step, after the scheduled event has been executed.

This can be useful e.g. to check if some model variable is within the allowed range.

Monitor functions can be dynamically added and deleted.

Monitor functions are executed in the context of the simulator and get called without arguments.

See add_monitor() and delete_monitor().

Using a model monitor in a Stimulation Program

Moddy 1.10 introduced the wait_for_monitor() method to suspend the thread until the monitor returns True.

Example:

class MyThread1(moddy.VSimpleProg):
    def __init__(self, sim ):
        super().__init__(sim=sim, obj_name='Thread', parent_obj=None)


    def run_vthread(self):
        cycle = 0
        while True:
            self.busy(30, 'DEL#%d' % cycle)
            self.wait(10)
            cycle += 1

class StimThread(moddy.VSimpleProg):
    def __init__(self, sim, supervised_thread ):
        super().__init__(sim=sim, obj_name='Stim', parent_obj=None)
        self.supervised_thread = supervised_thread

    def run_vthread(self):
        self.wait_for_monitor(None, self.monitor_func1)
        self.annotation('got mon1')
        self.wait_for_monitor(None, self.monitor_func3)
        self.annotation('got mon3')
        if self.wait_for_monitor(10, self.monitor_func1) == 'timeout':
            self.annotation('tout waiting for mon1')

    def monitor_func1(self):
        # called in the context of the simulator!
        return self.supervised_thread._state_ind == "DEL#1"

    def monitor_func3(self):
        # called in the context of the simulator!
        return self.supervised_thread._state_ind == "DEL#3"

simu = moddy.Sim()

t1 = MyThread1(simu)

stim = StimThread(simu, t1)

simu.run(200)