Demo Calculator

Electronic Calculator

The Calculator demo, modeling a simple electronic calculator, is inspired by the example in the book book "Practical UML Statecharts in C/C++, Second Edition - Event-Driven Programming for Embedded Systems" by Miro Samek, ISBN: 978-0-7506-8706-5. The reason for including this demo is to compare the models of both approaches.

Generally speaking, the big advantage of Dr. Samek's approach is performance concerning execution speed and footprint. An application is extremely fast thanks to among others the programming language C/C++, the provided, highly optimised state machine framework library, and the shortcuts taken in the state transitions. Dr. Samek's dedicated state modeling tool, refer to www.state-machine.com, is able to generate C/C++ source code and verify the state machines.

Please, compare the layout of the following 2 Finite State Machines. Note that in TismTool's FSM below the operand1 and operand2 composite states are realised by SubMachines, avoiding duplication in modeling and in source code. Furthermore, TismTool's FSM is crowdy since it contains all code activities (mostly delegated to object View).

Dr. Samek's FSM :

Miro Samek Calculator

TismTool's FSM :

TismTool Calculator

As a second alternative approach, the ASD:Suite of Verum has been applied for modeling the Calculator state logic. The interface/design state machines have been verified successfully; and Java source code has been generated. This VCalc_Java.zip file contains all models and the full Eclipse project including the generated and the manual source code; it also contains a pdf of the design model, the resulting SVG design state machine diagram, and the executable jar of the console application.
Two modeling changes were needed compared to the UML model:
1. A 'boot' state has been added. ASD lacks the feature of entry/exit actions. The entry action of the 'begin' state is realised at the transition from 'boot' to 'begin'. Also other entry actions need to be executed during transitions.
2. The operation 'OperMinus()' has been added. In ASD function parameters (like operId) can not be used in guards. A guard for checking operId being '-' could be implemented in the Calculator design model by a foreign boolean function. However, that resulted in a mismatch between the design model and its interface model (that can not rely on such a foreign function). As a consequence the client component has to differentiate between 'Oper()' and 'OperMinus()' , emphasizing quite rightly the essential differences between these functions.
The ASD:Suite has also been used to generate source code in C++ . This VCalc_Cpp.zip file contains the models, Microsoft Visual C++ 2008 Express project settings, the generated and the manual source code, and the console executable VCALC.exe . Note that the models for C++ have a minimal difference compared to the models for Java, because of the usage of the programming language depending string type in 2 function parameters.

Valid combinations for generating source code from the UML model by TismTool are in the table below.

Target

Generate

Protocols


CalculatorProtocol

Simulation code, Verification code

Architecture


ExecEnv

Simulation code, Verification code

ExecEnv_Kbd

Source code + main, yielding a Console Application

ExecEnv_Ui

Source code (for C# and Java)
N.B. For C# : Change Visual Studio project properties of tab Application to: Output type equal to Windows Application and Startup object equal to Calculator.Program

The character input for the ExecEnv_Kbd console application are 10 digits, . (digital dot), =, 4 operators , c (cancel, also after error), e (clear entry), and q (quit). For the Java and C++ application (unlike the C# application) after each character the Return key must be pressed.

The file TismSds.html contains an overview of the verification scenarios.

The files in the tables below are free to download.

C# source code generation

Calculator.xml The XMI file of the Calculator UML model.
Calculator.tsm The project file for the TismTool.
CalculatorTranslations.tsl
The translation table.
Calculator.pdf The UML diagrams.
Calculator.zip The zipped archive containing the (generated) source code, the UI executable, and the logfiles TismLog_0001.txt and TismSeq_0001.txt of the protocol verification.
AllCalculator.zip All the above files zipped together.

Java source code generation

Calculator.xml
The XMI file of the Calculator UML model.
Calculator_Java.tsm
The project file for the TismTool.
CalculatorTranslations_Java.tsl
The translation table.
Calculator.pdf
The UML diagrams.
Calculator_Java.zip The zipped archive containing the (generated) source code, the UI executable jar, and the logfiles TismLog_0001.txt and TismSeq_0001.txt of the protocol verification.
AllCalculator_Java.zip All the above files zipped together.

C++ source code generation (Windows)

Calculator_Cp.xml
The XMI file of the Calculator UML model.
Calculator_Cpp.tsm
The project file for the TismTool.
CalculatorTranslations_Cpp.tsl
The translation table.
Calculator_Cp.pdf
The UML diagrams.
CalculatorInclude.hpp Include file inserted in TsmSystem.h .
Calculator_Cpp.zip

The zipped archive containing the (generated) source code, the console executable, and the logfiles TismLog_0001.txt and TismSeq_0001.txt of the protocol verification. The used C++ Boost library has version 1.48 .

AllCalculator_Cpp.zip
All the above files zipped together.

C++ source code generation (Linux)

L_CALCULATOR_CPP.tar.gz

The tar-zipped archive containing the (generated) source code, the makefiles, the console executable, and the logfiles TismLog_0001.txt and TismSeq_0001.txt of the protocol verification. The used C++ Boost library has version 1.47 .

L_AllCALCULATOR_CPP.tar.gz
The tar-zipped archive containing the XMI file of the Calculator UML model, TismTool project file, the include file, the translation table, pdf of UML diagrams, and the above L_CALCULATOR_CPP.tar.gz file.

C source code generation (Windows)

Calculator_Cp.xml
The XMI file of the Calculator UML model.
Calculator_C.tsm
The project file for the TismTool.
CalculatorTranslations_C.tsl
The translation table.
Calculator_Cp.pdf
The UML diagrams.
Calculator_C.h Include file inserted in TsmSystem.h .
Calculator_C.zip

The zipped archive containing the (generated) source code, the console executable, and the logfiles TismLog_0001.txt and TismSeq_0001.txt of the protocol verification. The used OSAL library is based on Windows.

AllCalculator_C.zip
All the above files zipped together.

C source code generation (Linux)

L_CALCULATOR_C.tar.gz

The tar-zipped archive containing the (generated) source code, the makefiles, the console executable, and the logfiles TismLog_0001.txt and TismSeq_0001.txt of the protocol verification. The used OSAL library is based on Linux.

L_AllCALCULATOR_C.tar.gz
The tar-zipped archive containing the XMI file of the Calculator UML model, TismTool project file, the include file, the translation table, pdf of UML diagrams, and the above L_CALCULATOR_C.tar.gz file.

Discussion

TismTool reports the following remarks about the UML model:

E 2395: No Fsms @ class ( Xmi > Data > Repository > Keyboard > KbdClass )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorServer > CalculatorServerPsm >> CompoundState >> ChoiceState )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorServer > CalculatorServerPsm >> CompoundState >> ChoiceState )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm >> CompoundState )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm > OperandXClientPsm >> CompoundState >> zero )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm > OperandXClientPsm >> CompoundState >> int )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm > OperandXClientPsm >> CompoundState >> int )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm > OperandXClientPsm >> frac )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm > OperandXClientPsm >> frac )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm > OperandXClientPsm >> frac )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm >> CompoundState >> CompoundState >> negated1 )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm >> CompoundState >> CompoundState >> negated2 )

ad E 2395:
The behaviour is implemented in the foreign View object via the overridden TsmRun().

ad I 4360:
Informal guards are translated to source code depending on the purpose. For verification/simulation the guard becomes a condition that is dynamically true of false to generate all possible scenarios. Generating application code for a protocol is not very meaningful, and the guard becomes always 'true'.

ad W 4535:
Self-transitions may cause an unlimited number of messages to a receiver causing queue overflow.

Verification CalculatorProtocol:

The verification of the CalculatorProtocol reports one deadlock situation, that is in fact not a deadlock. This situation happens when the trigger Off() causes a transition to a final state.
Due to the absence of any triggers, including NativeTriggers, from the final state the situation is considered as deadlock. Refer to this scenario.

By downloading and/or using the above items you accept the terms of the Disclaimer. So make sure you have read it before downloading or using anything from this section of the site. In general terms that means you use them at your own risk, and we accept NO RESPONSIBILITY WHATSOEVER for anything that may occur as a result of your use of, or inability to use, any item provided via these pages.

E 2395: No Fsms @ class ( Xmi > Data > Repository > Keyboard > KbdClass )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorServer > CalculatorServerPsm >> CompoundState >> ChoiceState )
I 4360: Informal guard "ok" becomes 'true' @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorServer > CalculatorServerPsm >> CompoundState >> ChoiceState )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm >> CompoundState )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm > OperandXClientPsm >> CompoundState >> zero )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm > OperandXClientPsm >> CompoundState >> int )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm > OperandXClientPsm >> CompoundState >> int )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm > OperandXClientPsm >> frac )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm > OperandXClientPsm >> frac )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm > OperandXClientPsm >> frac )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm >> CompoundState >> CompoundState >> negated1 )
W 4535: Self-transition is errorprone for NativeTrigger @ ( Xmi > Data > Protocols > CalculatorProtocol > CalculatorClient > CalculatorClientPsm >> CompoundState >> CompoundState >> negated2 )