Menu

Tree [d9aa4e] master /
 History

HTTPS access


File Date Author Commit
 core 2023-09-05 Tomas Prerovsky Tomas Prerovsky [cc10e3] [OBLECTAMENTA-VM][VMLANG][FEATURE] Function cal...
 crawler 2015-10-02 Tomas Prerovsky Tomas Prerovsky [ed9773] Initial commit of version 0.1 sources.
 demo 2017-04-11 ceps ceps [c315b4] [FEATURE] demo/hello_world
 doc 2023-06-25 Tomas Prerovsky Tomas Prerovsky [3f624c] [BUGFIX][DOCGEN] Segmentation fault if statemac...
 examples 2023-09-14 Tomas Prerovsky Tomas Prerovsky [4ce731] Example for fetching data recursively.
 ide_support 2015-10-02 Tomas Prerovsky Tomas Prerovsky [ed9773] Initial commit of version 0.1 sources.
 import-scripts 2020-12-17 Tomas Prerovsky Tomas Prerovsky [6146fb] Moving stuff
 include 2015-10-02 Tomas Prerovsky Tomas Prerovsky [ed9773] Initial commit of version 0.1 sources.
 jit 2018-06-08 ceps ceps [e6f2c4] Qt project file for jit project added
 qt 2017-12-01 ivanbr ivanbr [774102] [FEATURE] DBC Import Script: Lexer now reads de...
 src 2022-10-13 Tomas Prerovsky Tomas Prerovsky [0e1cb6] [FEATURE] Option --root_struct .
 test 2022-11-22 Tomas Prerovsky Tomas Prerovsky [ee9be7] [VM][Oblectamenta] Testbench, basic declarations.
 tools 2021-05-21 Tomas Prerovsky Tomas Prerovsky [14b2b9] [FEATURE][TOOLS][PLTSQ]Experiments with svg.
 utils 2021-11-24 Tomas Prerovsky Tomas Prerovsky [459d82] Some refactoring of action execution.
 visual_studio 2015-11-19 cepsdev cepsdev [1c3816] [BUGFIX] changed() works in interplay with CAL ...
 vm 2023-09-05 Tomas Prerovsky Tomas Prerovsky [cc10e3] [OBLECTAMENTA-VM][VMLANG][FEATURE] Function cal...
 .gitattributes 2017-08-23 ceps ceps [2a03d2] [FEATURE] CAN MAPPING TOOL FOR WINDOWS
 .gitignore 2022-01-05 Tomas Prerovsky Tomas Prerovsky [242ea0] Remove studies
 INSTALL.md 2023-09-16 Tomas Prerovsky Tomas Prerovsky [d9aa4e] Update INSTALL.md
 LICENSE 2021-03-03 Tomas Prerovsky Tomas Prerovsky [12df07] License updated
 Makefile 2022-11-09 Tomas Prerovsky Tomas Prerovsky [cbbcf0] [VM] Embarrassing benchmark results.
 README.md 2023-06-25 Tomas Prerovsky Tomas Prerovsky [cff674] Update README.md
 contributors.txt 2015-10-02 Tomas Prerovsky Tomas Prerovsky [45154d] Initial commit with contributors.
 make_machines.sh 2021-04-18 Tomas Prerovsky Tomas Prerovsky [ec3e64] [BUGFIX] Building ceps with parallelization fails.

Read Me

machines4ceps

Write, run, and trace complex state machines (UML statecharts, Harel statecharts, state diagrams).

ceps

Machines4ceps is part of the ceps tool. The name ceps is derived from the word 'spec' - the abbreviation of specification - spelled backwards.
Ceps is pronounced like the word 'caps' which is (almost) the phonetical reverse of spec. The idea behind ceps is that a correct real world specifcation
can only be derived by following a bottom up approach. Ceps is part of a bigger methodology called 'corpus based software engineering' which is a manifestation of a version of Nietzschean philosophy geared towards a world ruled by software. Stated in a few words: ceps is about freedom and how to keep it.

Installation

Details can be found here

Writing and running state machines - Quick Start

This intro follows closely the discussion in https://en.wikipedia.org/wiki/UML_state_machine.

A basic state machine

Basic state machine
Source:Wikipedia

A basic state machine: Notation

Here comes our very first version of the depicted state machine:

kind Event;

Event CAPS_LOCK, ANY_KEY;

sm{
 basic_example;

 states{Initial; default; caps_locked;};

 t{Initial;default;}; 
 t{default;caps_locked;CAPS_LOCK;};
 t{caps_locked;default;CAPS_LOCK;}; 
};

The notation is a bit clumsy but readable. The code can be found in examples/first_steps/basic_uml_state_diagram.ceps.

Yes, machines4ceps is all about coding state machines, the drawing is - or at least should be - done by algorithms (see the section on drawing state machines). This approach has two major benefits:
- it scales, a purely graphical approach isn't feasible if your system has thousands of states.
- it is compatible with the established methods and tools we use to write software in general.

A basic state machine: Execution (Part I)

One way to understand what a state machine is doing is to run a simulation. Simulating state machines is a key feature of machines4ceps.
To get our example running the only thing we need to add is a Simulation directive including a Start directive with the names of the state machines we want to run:

Simulation{
 Start{basic_example;};
 };

To run this example, open a shell/terminal, change your working directory to the machines4ceps repo, and type:
* cd examples/first_steps
* ../../bin/ceps basic_uml_state_diagram.ceps simulation_1.ceps

After executing the last command, you should get the following output:

basic_example.Initial- basic_example.default+

The meaning of which is, that the machine basic_example made a single transition from the initial state Initial to the state default.

A basic state machine: Execution (Part II)

Let's fire three CAPS_LOCK events and look how the state machine behaves.

Simulation{
 Start{basic_example;};

 CAPS_LOCK;
 CAPS_LOCK;
 CAPS_LOCK;
 };

To run this simulation, open a shell and type (assuming your working directory is machines4ceps/examples/first_steps):
* ../../bin/ceps basic_uml_state_diagram.ceps simulation_2.ceps

This should produce the following output:

basic_example.Initial- basic_example.default+
basic_example.default- basic_example.caps_locked+
basic_example.default+ basic_example.caps_locked- 
basic_example.default- basic_example.caps_locked+

The default behaviour of ceps is approximately as follows: fetch an event, process all transitions triggered by that event, report the set of affected states, and repeat. If we run our simulation inside a terminal window, ceps will report the set of changed states by simply printing the name of each state followed by a + or -, indicating whether the state is active or not (this notation was introduced by Arne Kirchhoff). Each iteration produces one line of output. We have three events in our last simulation, but four lines of output.That's because of the transition t{Initial;default;}; which has no associated event and is therefore triggered simply by starting the state machine (epsilon transition).

Visualization (The --dot_gen option)

The following requires graphviz to be installed on your machine (see https://graphviz.org).

With the option --dot_gen set, ceps writes a dot representation of all top level state machines into the file out.dot.

The commands

  • ../../bin/ceps basic_uml_state_diagram.ceps --dot_gen
  • dot -Tpng out.dot -o img/basic_uml_state_diagram.png

produce the following graphical representation of the state machine basic_example.

Visualization (The --pr option)

Another possibility, which requires nothing else than a shell, offers the --pr option. It outputs a python like representation on stdout.

The commands

  • ../../bin/ceps basic_uml_state_diagram.ceps --pr

produce the following output on the console:

Completing the basic example: Adding Actions

We complete the ceps version of the basic state machine, by adding the missing transitions under the ANY_KEY event together with the associated actions.

kind Event;

Event CAPS_LOCK, ANY_KEY;

sm{
 basic_example;
 states{Initial; default; caps_locked;};

Actions{
  send_lower_case_scan_code {print("basic_example.send_lower_case_scan_code()\n");};
  send_upper_case_scan_code{print("basic_example.send_upper_case_scan_code()\n");};
 };

 t{Initial;default;};
 t{default;caps_locked;CAPS_LOCK;};
 t{caps_locked;default;CAPS_LOCK;};

 t{default;default;ANY_KEY;send_lower_case_scan_code;};
 t{caps_locked;caps_locked;ANY_KEY;send_upper_case_scan_code;};
};


The code can be found in examples/first_steps/basic_uml_state_diagram_with_actions.ceps.

The extended version works perfectly fine with our simulations (simulation_1.ceps and simulation_2.ceps) developed so far, and exhibits exactly the same behaviour as our previous version under the current set of simulations. To get a somehow different behaviour, we need to trigger at least one ANY_KEY transition. That's done
by adding a couple of ANY_KEY events to our simulation.

Simulation{
 Start{basic_example;};

 ANY_KEY;
 CAPS_LOCK;
 ANY_KEY;
 CAPS_LOCK;
 ANY_KEY;

 };

The code can be found in examples/first_steps/simulation_3.ceps.

If we run

  • ../../bin/ceps basic_uml_state_diagram_with_actions.ceps simulation_3.ceps

we get the following output.

basic_example.Initial- basic_example.default+ 
basic_example.send_lower_case_scan_code()
basic_example.default- basic_example.caps_locked+ 
basic_example.send_upper_case_scan_code()
basic_example.default+ basic_example.caps_locked- 
basic_example.send_lower_case_scan_code()

Communication via WebSockets

One of the supported protocols is WebSocket (https://en.wikipedia.org/wiki/WebSocket).

The option --ws_api PORT

The option --ws_api PORT, where port is a 16 bit unsigned integer, will start ceps as a WebSocket server listening on port PORT. This allows us to send and receive events, set values etc. remotely via the WebSocket API.

Running the basic example as a WebSocket server

Run

 ../../bin/ceps basic_uml_state_diagram_with_actions.ceps empty_simulation.ceps --ws_api 3001

Open a second shell/terminal, and run websocat (https://github.com/vi/websocat):

 websocat ws://localhost:3001

If you type

 EVENT CAPS_LOCK

You should observe a transition to the state basic_example.caps_locked, i.e the shell running the state machine should produce the output

basic_example.default- basic_example.caps_locked+ 

Extended States and guards

Extended States

State machines combined with variables holding values, like integers, strings etc., are called extended state machines (see https://en.wikipedia.org/wiki/UML_state_machine#Extended_states). We call extended states Systemstate.
Extended states are introduced, or declared, using the notation

Systemstate variable_name;

kind Event;
kind Systemstate;

Systemstate key_count;

Event CAPS_LOCK, 
      ANY_KEY;


sm{
 basic_example;

 states{Initial; 
        default; 
        caps_locked;};

 on_enter{
     key_count = 10;
 };

 Actions{
  send_lower_case_scan_code {
     key_count = key_count - 1; 
     print("key_count=",key_count,"\n");
  };
  send_upper_case_scan_code{
     key_count = key_count - 1;
     print("key_count=",key_count,"\n");
  };
 };

 t{Initial; default;};
 t{default; caps_locked; CAPS_LOCK;};
 t{caps_locked; default; CAPS_LOCK;};

 t{default; default; ANY_KEY; send_lower_case_scan_code;}; 
 t{caps_locked; caps_locked; ANY_KEY; send_upper_case_scan_code;};
};

The code can be found in examples/first_steps/extended_uml_state_diagram_with_actions.ceps.

To run this example, open a shell/terminal, change your working directory to the machines4ceps repo, and type:
* cd examples/first_steps
* ../../bin/ceps extended_uml_state_diagram_with_actions.ceps simulation_3.ceps

This will generate the following output:

basic_example.Initial- basic_example.default+ 
key_count=9
basic_example.default- basic_example.caps_locked+ 
key_count=8
basic_example.default+ basic_example.caps_locked- 
key_count=7

Setting up preconditions/ensuring invariants: on_enter

Some definitions

(skip this if you are not into details)

In order to give a sufficiently precise explanation of on_enter we need a couple of
more fundamental definitions first.

The single most important structure, when it comes to the execution of a state machine, is the active states set.

A state is active exactly if it is in the active states set or ASS, a state is inactive if it is not active,
i.e. not a member of the active states set. The ASS is intially empty, a command like
Start{NameOfStateMachine;}; puts, conceptually speaking, the state referred to by NameOfStateMachine in the active states set.
Yes, a state machine is a state. States with an inner structure - like state machines - are called composite states.

If an inactive state becomes active, i.e. a state which is not in the ASS being put into the ASS, we say the state is being entered. A state is being visited if it is added to the ASS, this includes the case of the state being already in the ASS. A state being entered is also visited, but you can visit a state without entering it.

A state machine is started by entering it, e.g. the previously mentioned Start{NameOfStateMachine}; command enters the (composite) state referred to by NameOfStateMachine.

Another important notion is the set of active transitions SAT(s,E) . This is - roughly - the set of all transitions of the form t{s;.;E;...}; for a state s and an event E.

Execution of a state machine

(skip this if you are not into details)

Conceptually the execution of a state machine follows the following schema - very approximate :

  • While ASS is not empty do
  • Fetch an event E
  • L := []
  • for each state s in ASS do
    • for each transition t{s,s',E,actions,guards} in SAT(s,E) with at least one true g in guards do
      • L += [s']
      • Run each action in actions
      • if s' is not in ASS call s'.on_enter (A)
  • OLD_ASS = ASS
  • N = set of all s in OLD_ASS with no transition under E
  • ASS = L + N
  • Exited := OLD_ASS - ASS
  • for each state s in Exited do
    • call s.on_exit (B)

Especially steps (A) and (B) don't tell the whole truth.

on_enter, on_exit

A state machine can define a special action on_enter which is called when the state machine is entered, i.e visted the very first time.
The purpose of on_enter is the same as that of contructors in C++: to setup invariants.
In the case a state machines is exited a potential on_exit routine is called.

Example:

kind Event;
kind Systemstate;

Event E;

sm {
 S;
 on_enter{
  print("S.on_enter()\n");
 };

 sm{
   T;
   on_enter{
    print("T.on_enter()\n");
   };
   on_exit{
    print("T.on_exit()\n");
   };
   states{Initial;};
 };

 sm {
  U;
  on_enter{
   print("U.on_enter()\n");
  };
  states {Initial;};
 };

 states{Initial;};
 t{Initial;T;};
 t{T;U;E;};
};

Simulation{
 Start{S;};
 E;
};

The code can be found in examples/first_steps/exit_enter_handlers.ceps.

To run this example, open a shell/terminal, change your working directory to the machines4ceps repo, and type:
* cd examples/first_steps
* ../../bin/ceps exit_enter_handlers.ceps

Output is:

S.on_enter()
T.on_enter()
S.Initial- S.T+ S.T.Initial+ 
T.on_exit()
U.on_enter()
S.T- S.T.Initial- S.U+ S.U.Initial+ 

Guards

kind Event;
kind Systemstate;
kind Guard;


Guard g1,g2;

g1 = 1 < 2;
g2 = 1 > 2;

Event E;

sm{
 S;
 states{Initial;a;b;c;};
 t{Initial;a;g1;};
 t{a;b;E;g2;};
 t{a;c;E;!g2;};
};

Simulation{
 Start{S;};
 E;
};

Output:

S.Initial- S.a+ inalizing 
S.a- S.c+ 

Finalizing the introductory example

kind Event;
kind Systemstate;
kind Guard;



Event CAPS_LOCK,
      ANY_KEY;
Systemstate key_count;

Guard g,not_g;
g = key_count == 0;  
not_g = !g;

sm{
 basic_example;

 states{Initial;
        default;
        caps_locked;
        Final;};

 on_enter{
     key_count = 10;
 };

 Actions{
  send_lower_case_scan_code {
     key_count = key_count - 1;
     print("key_count=",key_count,"\n");
  };
  send_upper_case_scan_code{
     key_count = key_count - 1;
     print("key_count=",key_count,"\n");
  };
 };

 t{Initial; default;};
 t{default; caps_locked; CAPS_LOCK;};
 t{caps_locked; default; CAPS_LOCK;};
 t{default;Final;ANY_KEY;g;};
 t{caps_locked;Final;ANY_KEY;g;};
 t{default; default; ANY_KEY;not_g; send_lower_case_scan_code;};
 t{caps_locked; caps_locked; ANY_KEY;not_g; send_upper_case_scan_code;};
};

A Calculator

kind Event;
kind Systemstate;
kind Guard;


Event DigitOrDot, Equals, Operator, C, OFF;

sm{
 calculator;
 states{Initial;Final;};
 sm{
  on;
  on_enter{
   print("on.on_enter()\n");
  };
  states{operand1;opEntered;operand2;result;Initial;};

  t{Initial;operand1;};
  t{operand1;operand1;DigitOrDot;};
  t{operand1;opEntered;Operator;};
  t{opEntered;operand2;};
  t{operand2;operand2;DigitOrDot;};
  t{operand2;result;Equals;};
  t{result;operand1;};
 };

 t{Initial;on;};
 t{on;on;C;};
 t{on;Final;OFF;};
};


Simulation{
 Start{calculator;};
 DigitOrDot;
 DigitOrDot;
 Operator;
 C;
 DigitOrDot;
 OFF;
};

Source in examples/first_steps/calculator.ceps.

Output:

on.on_enter()
calculator.Initial- calculator.on+ calculator.on.Initial+ 
calculator.on.operand1+ calculator.on.Initial- 
calculator.on.operand1- calculator.on.opEntered+ 
calculator.on.opEntered- calculator.on.operand2+ 
calculator.Final+ calculator.on- calculator.on.operand2-