%% Power Window Controller Temporal Properties
% This example shows how to model temporal system requirements in a power window
% controller model for property proving and test case generation using 
% Simulink(R) Design Verifier(TM) Temporal Operator blocks.

% Copyright 2009-2014 The MathWorks, Inc.


%% Temporal Operators
% The <matlab:open_system('sldvlib') Simulink(R) Design Verifier(TM) library>
% provides three basic temporal operator blocks which can be used to model temporal properties.
% The intent of the temporal operators is to support the 
% specification of temporal requirements, such that the modeled property
% has a closer correlation to the actual textual requirement. These blocks
% are low-level building blocks for constructing more complex temporal 
% properties. 


%% Power Window Controller
% The power window controller responds to the driver and passenger commands
% by giving the commands for moving the window up or down. It also responds
% to an obstacle and to reaching the end of the window frame in either
% direction. 
% 
% Consider the following two requirements for the power window controller:
%
% *Requirement 1 (Obstacle Response)*
%
% Whenever an obstacle is detected, the controller shall give the
% down command for 1 second.
%
% *Requirement 2 (AutoDown feature)*
%
% If the driver presses the down button for less than 1 second, the
% controller keeps giving the down command until the end has been reached or 
% the driver presses the up button.
%

%Model of the power window controller
open_system('sldvdemo_powerwindowController')
open_system('sldvdemo_powerwindowController/control')


%% Property Specification
% The power window verification system is the top-level model that contains
% a model reference to the power window controller model specifying the 
% controller behavior and the modeled requirements.

%Model of the top-level verification system
open_system('sldvdemo_powerwindow_vs')


%%
% *Global Assumptions:*
% The power window controller is an open system. This makes the 
% environment controlled inputs, obstacle and endstop (end of the window 
% frame) to occur freely. To constrain the environment, add two global
% assumptions for your controller model. 
%
% 1) The obstacle and the endstop inputs never become 
% true at the same time.
% 
% 2) The obstacle does not occur multiple times within the following 
% 1-second interval.
%
% For the temporal assumption on obstacle, use a Detector block
% with output type of "Delayed Fixed Duration" to capture the fixed
% duration of 1 second (5 time steps with 0.2 sample time).

% Global Assumptions
open_system('sldvdemo_powerwindow_vs/Global Assumptions')


%%
% Now consider the first controller requirement for *Obstacle Response*.
%

% Obstacle Response
open_system('sldvdemo_powerwindow_vs/Verification Subsystem2')


%%
% Here, use the Detector block with output type of "Delayed Fixed 
% Duration" for the property specification. After detection of the 
% obstacle, construct a fixed interval of 4 steps. Note
% that the input is not observed during the output construction phase for
% the Detector with "Delayed Fixed Duration" output type. In the case 
% where the obstacle can occur freely in absence of the assumption, 
% you might wish to observe all the intermediate occurrences of the obstacle. This can 
% be achieved through an Extender block with "Finite" extension duration 
% of 4 time steps.
%
% Now consider the *AutoDown feature* of the power window controller.
%
% <<powerwindow_Prop3_False.PNG>>
%
% For illustration, consider this property specification in 
% smaller parts:
%
% # The first temporal duration of interest, "driver presses the down 
% button for less than 1 second", is captured by Detector1. At sample rate
% of 0.2, the 1-second interval is broken down into 5 time steps.
% On detection of the down signal, Detector1 constructs a 5-step fixed temporal
% duration at its output, which you will subsequently use in
% combination with other constraints. 
% # For the AutoDown feature, you know that the down
% signal cannot be pressed for more than 1 second, or 5 time steps. Thus,
% you want to ensure that both driver up and down are "true"
% or both are "false" in less than 5 steps after down is 
% pressed. By taking the AND of this driver neutral and the 
% Detector output, enforce the constraint that driver down can
% be pressed for any number of consecutive time steps less than 5.
% # You also need to ensure that, during this period, other signals such as 
% obstacle, EndStop and DriverUp are not true, since these will take 
% the controller out of responding to the down press. This is captured using 
% Detector2 by enforcing that NOT(HaltDown) is true for 5 time steps.
% Detector2 has "Delayed Fixed
% Duration" output type. It also has "Time steps for input detection" = 5 and "Time steps 
% for output duration" = 1.
% # Take the AND of these constructed durations.
% # For the AutoDown feature, you do not want to limit the number of time 
% steps for which the controller gives the down command. You
% know that you want the controller to keep giving the down command as long
% as the driver does not press an up or down command again, or an
% obstacle or the physical end of the window frame is not hit. This behavior can be
% captured by the Extender block with "Infinite" extension period and an
% external reset signal that encodes the condition to end the
% extension. 
% # The final piece is an Implies block that takes the temporal duration
% constructed as explained above and checks if the controller down command
% is true for every time step of this duration. 
%
% Once you have this initial property specification, you can use it for 
% property proving with Simulink Design Verifier. You will get a
% counterexample for this property. The counterexample shows a scenario
% where the down command is given when the controller was in the emergency 
% down state due to the response to an earlier detected obstacle. After you add a
% constraint to avoid this, you will get another counterexample: if the down 
% button is pressed when previously the up command was being 
% given, the AutoDown feature is disabled and the down command is given
% only as long as the down button is pressed. Looking at these
% counterexamples and observing the model, you can see a pattern that the 
% AutoDown feature is enabled only when the controller is in a neutral state
% to begin with when the driver presses the down button.
%
% Incorporate this constraint by forcing the controller output to be 
% neutral - neither up nor down command is true - as a precondition for the 
% AutoDown property. This property is proven valid.

% Valid AutoDown
open_system('sldvdemo_powerwindow_vs/Verification Subsystem3')


%% Test Case Generation for Property Validation
% Once the properties are specified, in addition to property proving, you 
% can run Simulink Design Verifier to automatically generate test cases
% that exercise various conditions in the property. This can be achieved 
% by placing custom Test Objective blocks at appropriate locations in the 
% property.
%
% One such location to place a Test Objective block (with "true" value) is on the
% signal feeding into the first input of the Implies block (as shown in the
% above property). On running test generation, this Test Objective is
% satisfied and you will get a test case exercising the various constraints
% encoded in the property. Simulink 
% Design Verifier can also create a test harness to simulate this test case.
% The Signal Builder block with relevant signals is shown below.
%
% <<powerwindow_Prop3_TC.PNG>>
% 
% One can now simulate this test case, and see how the temporal durations
% are created in the property by placing a scope that displays the input
% and output values of the two Detector blocks and No_Cmd.
%
% <<powerwindow_Prop3_S.PNG>>
% 
% Manually inspecting the test case values enables you to see if the 
% specified property behaves as intended. 
%
% This Test Objective block helps in identifying a scenario where the property is
% valid while the Implies block is not trivially true. An Implies block is trivially 
% true when its output is true because of its first input being false. 
% When you get a test case satisfying this Test Objective, 
% you know that there is at least one case where the first input to the 
% Implies block is true.
%
% This exercise can help you validate your property specifications by
% manually inspecting the test cases automatically generated by Simulink
% Design Verifier.

%% Clean Up
% To complete the example, close all the opened models. 

close_system('sldvdemo_TOBlocks',0);
close_system('sldvdemo_powerwindowController',0);
close_system('sldvdemo_powerwindow_vs',0);


displayEndOfDemoMessage(mfilename)
