Keypad Processing - lgwagner/SpeAR GitHub Wiki
This component handles how the time entry of the display in conducted. Using a simple microwave oven, the digit pressed on the keypad is always added to the right-hand end of the term with all numbers being shifted left. This is the case in in this example.
Note- One may notice that should the keypad continue to be pressed (beyond three digits) the pressed digit will continue to enter the right side of the value and push off the left-most value. This is okay for this example but perhaps this is not desirable. Challenge - Change the example to deny input when all digits are filled.
In this component it is only necessary to have access to the the global data types.
This component uses the user_input_type to capture the keypad entries. Looking closely at that enumeration, one may notice that there is a NULL entry. Since this analysis conducts synchronous validation then when the keypad is not being pressed is still an entry to the keypad processing component.
.png)
The outputs of this component provides the left, middle, and right digits to the display.
These macros provide easy to access reach back to the previous values of the left, middle, and right digits in the display. It is worth noting a particular aspect of the previous keyword. When a user uses previous it is often a good idea (but not required) to also use the with initial value form of the statement. This is because at the first time step the previous has no historical value and therefore can be manipulated by the model checker to be anything that would invalidate the system. The user can fully define this call with the use of with initial value which informs the model checker that at the first time step if a previous is requested this is the value. Essentially, this is an assumption established by the user for a particular case.
All of these requirements manage how the data entered into the keypad is stored in the system.
The properties here ensure that the values in all of the digit locations are valid.