sf_tlafter (Simulink model) Open this Model

Temporal Logic using the AFTER function

This simple demonstration compares the difference between two Stateflow charts: one chart uses temporal logic and the AFTER function to achieve the goal, and the other chart achieves the same goal without using temporal logic.

The AFTER function allows you to easily obtain the number of events that have occurred within that chart and then used as a condition for an event transition. For example, in this demonstration, a transition from the 'Off' to the 'On' state will occur after 10 events (labeled as 'secs') have passed as long as the input, 'step', is less than 1. In this case the input 'step' is created using a Step function block from Simulink and the event 'secs' is defined by using a Pulse Generator. The value of this step will be zero until 60 seconds of simulation have gone by. After 60 seconds pass, the step is created and the value of the step input is 1. Since one of the transition conditions in the chart is not met ('step' < 1) then the transition does not take place anymore and you can notice a halt in the chart activity.

The same effect is achieved without the use of temporal logic. The difference is that an additional variable and transition need to be included in order to count the number of times an event takes place. In this case, the local variable 'count_after' is used to obtain the number of times the event 'secs' occurs. The transition will then take place if 'count_after' is greater than 10 and the value of step (which is the input) is less than 1.