- Notifications
You must be signed in to change notification settings - Fork0
rsveldema/state_machine_DSL
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
This project contains a light-weight state machine DSL. A codegenerator generates C++ code from a state machine's description. Thegenerated C code is compact, and for use on embedded devices (STM32,PIC, Arduino, Raspberry PI, Kinetis, LPC, Nordic, etc. should all workusing std. C++ compilers).
The DSL also contains facilities for writing unit tests and forautomatic model checking.
The generated code has some facilities for extensions.Extensions exist for delayed sending of events and for model checking support.
// <modelcheckable> lets creates a model that extends the basic class with features// for modelchecking.machine Blinky <modelcheckable> {// declare events to stimulate the machine: event b1"button 1 pressed";// declare C/C++ vars: Led led1; initial state bootup { entry {// C extension in our DSL: transition blink1; } } state blink1 { entry {/* write C code here*/ } exit {/* more C code*/ } event b1 {// write more C code if b1 is triggered, i.e.:printf("ignoring button1 press, already in b1\n"); transition blink2; } ...
From the above example we can:* generate a C++ class with the appropriate states as nested classes.* a graphviz diagram* generate CUnit tests* test that the transition statement is the last statement in the code(to avoid illegal accessing the prior state after a state transition).
After your model, you can optionally specify a number of tests to run:
testsuite buttonBoiling { test simple { transition bootup; waitmillis(500);// wait for boot to complete emit button_on; waitsecs(1);// wait for event to be processed emit button_start; waitsecs(6);// wait for boiling waterassert self->trace.contains("ENTER STATE: finish_boiling"); self->trace.dump(); }}A simple explicit state model checker is included. It attempts allpossible interleavings of external events sent to the machine.For model-checking we suggest to use stubbed/mocked devices if your modelinteracts with devices.
#include"generated_state_machine_boiler.hpp"#include"../model_checker/model_check.h"intmain(int argc,char **argv){ WaterBoiler *p =newWaterBoiler();// from this state onwards we want to// try all possible event permutations sent: p->transition(p->state_union.bootup);// instantiate the model checker and run the test: Modelchecker<WaterBoiler>mc(p); mc.run();return0;}
For the model checker to work, the mocked devices must have 'operator <' definedand be safe to copy with a copy constructor.
* install graphviz* install python 3* install antlr 4* install cunit [ http://cunit.sourceforge.net ]* install astyle // used to make the generated code pretty, // disable if you want.* pip3 install antlr4-python3-runtime* pip3 install pystache* gcc g++* makeAntlr [http://www.antlr.org] then generates a parser from the DSL's grammar.Hence, first install python and antlr4 using your platform's installers.
src/dsl.antlr -- antlr grammar of DSL, generates dslParser.py, etc
src/generate.py -- generates the C++ code taking templates/* as input and -- replacing {{..}} with text fragments created here
src/stringify.py -- pretty prints the antlr AST
src/analyzer.py -- tests that a transition statement is the very last in an action block
templates/main.template.cc -- the main() function for CUnit unit tests
template.generated_code.h -- the frame for the generated state machine header file
examples/*.sm -- example state machines. We use cpp to allow #include statements to split larger state machines into several files
model_checker
About
state machine DSL
Topics
Resources
License
Uh oh!
There was an error while loading.Please reload this page.
Stars
Watchers
Forks
Releases
Packages0
Contributors2
Uh oh!
There was an error while loading.Please reload this page.