Belenos

Belenos is an ancient Celtic healing god... and, more anecdotally, a basic model checker that simulates the execution of a system model written in C.

Belenos consists in a single C header library. It is used to describe a system and check invariants on all reachable states.

A system is:

• a state (a C type)
• an initialization function (to set the initial state)
• a state print function
• a set of invariants (C functions returning boolean values)
• a set of liveliness conditions (C functions returning boolean values)
• a set of events (C function modifying states)

The Belenos engine builds a set of reachable states:

• the initial set contains the initial state
• for each new state, the engine applies all event functions -- one by one -- and produces new states
• for each liveliness condition, there shall be at least one valid reachable state satisfying this condition
• it stops when no new state can be reached

If all states satisfy all invariants and all goals are reached, the program successfully stops. Otherwise it prints the sequence of events that leads to the erroneous state.

The engine builds a breadth-first state graph. The erroneous event sequence is then (one of) the shortest path that leads to invalid states.

Additional simulations can be run to check that some specific states are reachable from non initial states.

Usage

C API

See belenos.h for further information.

MAX_EVENTS (macro)

Maximum number of events (user redefinable before including belenos.h)

MAX_INVARIANTS (macro)

Maximum number of invariants (user redefinable before including belenos.h)

MAX_GOALS (macro)

Maximum number of goals (user redefinable before including belenos.h)

MAX_STATES (macro)

Maximum number of states (user redefinable before including belenos.h)

struct state (type)

user defined type that shall be defined before including belenos.h.

INIT (macro)

Initial state description: The INIT macro declares a function that takes the initial state (struct state *q). It can initialize some or all fields of q. Unitialized fields are filled with null bytes.

PRINT (macro)

Print a state. The PRINT macro declares a function that takes a state to print (struct state *q). It is used to print the sequence of states and events that lead to erroneous states.

INVARIANT (macro)

Add an invariant. An invariant is a boolean function that takes a state and returns true if the invariant is satisfied.

GOAL (macro)

Add a goal. A goal is a boolean function that takes a state and returns true if the goal is satisfied. Goals are checked only on states that satisfy all the invariants.

EVENT (macro)

Add an event. An event is a function that takes a state and modifies it. Events are applied on states that satisfy all the invariants.

FROM, TO (macros)

Add a new path to be checked. FROM describes the new initial state. TO adds a new target state that must be reachable from the ne initial state. TO can be called several times to add multiple targets.

Scripts

Models are C programs. For faster development iterations, these programs can be run as shell scripts that compile and run themselves.

The trick is to write hybrid shell/C programs. The first line is a shell command that compiles and run the script, as well as a C comment ignored by the compiler.

E.g.:

demo.c:

//usr/bin/env cc -xc -Wall -O3 $0 -lm -o /tmp/$(basename $0) && exec /tmp/$(basename $0); exit $?
... C program here

The belenos shell script can also be used to execute Belenos scripts:

$ belenos script.c

Usage:

$ belenos --help

Usage: belenos [OPTIONS] <file>

Options:
  -h, --help          Print this help
  -s, --san           Enable sanitizers (ASan + UBSan)
  -l, --lib <lib>     Add a library
  -D<name>[=<value>]  Define a preprocessor macro
  -I<path>            Include path

Environment variables:
  CC                  C compiler (default: cc)

Examples:
  belenos main.c
  belenos -s -l libname -DDEBUG=1 main.c
  CC='zig cc' belenos --san --lib libname -DMAX_STATES=1000 main.c

Installation

install.sh installs belenos in $HOME/.local/bin and belenos.h in $HOME/.local/lib.

The installation prefix can be changed with the PREFIX environment variable:

$ PREFIX=/opt/belenos ./install.sh

Tutorial

This tutorial is a short example of a couple of traffic lights. The goal is to describe a system that ensures the traffic is allowed on both roads at the same time.

Naive model

The first model is pretty simple. It allows all color transitions and describes a safety invariant.

demo-0.c:

/* Traffic light system specification */

/* Traffic lights have three colors. */
enum traffic_light { GREEN, ORANGE, RED };

/* The system has two traffic lights. */
struct state {
    enum traffic_light l0;
    enum traffic_light l1;
};

/* The system state type shall be defined before including belenos.h */
#include "belenos.h"

/* The initial state has only red lights */
INIT {
    q->l0 = RED;
    q->l1 = RED;
}

/* Function used to print states in case of invariant violation */
PRINT {
    static const char *color[] = { [GREEN]="GREEN", [ORANGE]="ORANGE", [RED]="RED" };
    printf("light 0: %s -- light 1: %s\n", color[q->l0], color[q->l1]);
}

/* Safety invariant: the traffic can be authorized on one road only
 * => there is at most one green or orange light
 */
INVARIANT(one_green_or_orange_max) {
    int n = 0;
    if (q->l0 == GREEN || q->l0 == ORANGE) n++;
    if (q->l1 == GREEN || q->l1 == ORANGE) n++;
    return n <= 1;
}

/* Events for the first light */
EVENT(light_0_green)  { q->l0 = GREEN; }
EVENT(light_0_orange) { q->l0 = ORANGE; }
EVENT(light_0_red)    { q->l0 = RED; }

/* Events for the second light */
EVENT(light_1_green)  { q->l1 = GREEN; }
EVENT(light_1_orange) { q->l1 = ORANGE; }
EVENT(light_1_red)    { q->l1 = RED; }

This model is too simple. As expected the safety invariant is not satisfied. Here is a minimal event sequence that violates this invariant:

=======================================
model     : demo-0.c
---------------------------------------
invariants: 1
goals     : 0
events    : 6
paths     : 0
=======================================
Paths from the initial state
=======================================
Warning: one_green_or_orange_max: violated invariant
---------------------------------------
light 0: RED -- light 1: RED
>>> light_0_green
light 0: GREEN -- light 1: RED
>>> light_1_green
light 0: GREEN -- light 1: GREEN
Error: Invariant violation

Better model

To satisfy the safety invariant, a light can turn green or orange only when the other light is already red:

demo-1.c:

/* Events for the first light */
EVENT(light_0_green)  { if (q->l1 == RED) q->l0 = GREEN; }
EVENT(light_0_orange) { if (q->l1 == RED) q->l0 = ORANGE; }
EVENT(light_0_red)    {                   q->l0 = RED; }

/* Events for the second light */
EVENT(light_1_green)  { if (q->l0 == RED) q->l1 = GREEN; }
EVENT(light_1_orange) { if (q->l0 == RED) q->l1 = ORANGE; }
EVENT(light_1_red)    {                   q->l1 = RED; }

It shall be valid:

=======================================
model     : demo-1.c
---------------------------------------
invariants: 1
goals     : 0
events    : 6
paths     : 0
=======================================
Paths from the initial state
states    : 5
=======================================
Info: All invariants are satisfied in all reachable states.
Info: Each goal is satisfied in at least one reachable state.
Info: All paths have been successfully explored.

Even better model

The previous model is not perfect, it allows invalid (but safe) color transitions (e.g. GREEN -> ORANGE -> GREEN). To force and check allowed transitions, the model shall also contain the previous colors:

This example also adds liveliness requirements (goals) to check lights eventually turn green.

demo.c:

/* Traffic light system specification */

/* Traffic lights have three colors. */
enum traffic_light { GREEN, ORANGE, RED };

/* The system has two traffic lights (with their previous colors). */
struct state {
    enum traffic_light l0, l0_prev;
    enum traffic_light l1, l1_prev;
};

/* The system state type shall be defined before including belenos.h */
#include "belenos.h"

/* The initial state has only red lights */
INIT {
    q->l0_prev = ORANGE; q->l0 = RED;
    q->l1_prev = ORANGE; q->l1 = RED;
}

/* Function used to print states in case of invariant violation */
PRINT {
    static const char *color[] = { [GREEN]="GREEN", [ORANGE]="ORANGE", [RED]="RED" };
    printf("light 0: %s -> %s -- light 1: %s -> %s\n",
        color[q->l0_prev], color[q->l0], color[q->l1_prev], color[q->l1]);
}

/* Safety invariant: the traffic can be authorized on one road only
 * => there is at most one green or orange light
 */
INVARIANT(one_green_or_orange_max) {
    int n = 0;
    if (q->l0 == GREEN || q->l0 == ORANGE) n++;
    if (q->l1 == GREEN || q->l1 == ORANGE) n++;
    return n <= 1;
}

/* Allowed transitions */
INVARIANT(light_0_allowed_transitions) {
    return (q->l0_prev == GREEN  && q->l0 == ORANGE)
        || (q->l0_prev == ORANGE && q->l0 == RED)
        || (q->l0_prev == RED    && q->l0 == GREEN);
}
INVARIANT(light_1_allowed_transitions) {
    return (q->l1_prev == GREEN  && q->l1 == ORANGE)
        || (q->l1_prev == ORANGE && q->l1 == RED)
        || (q->l1_prev == RED    && q->l1 == GREEN);
}

/* Liveliness requirements */
GOAL(light_0_eventually_green) { return q->l0 == GREEN; }
GOAL(light_1_eventually_green) { return q->l1 == GREEN; }

/* Fairness */
GOAL(light_0_eventually_red) { return q->l0 == RED; }
GOAL(light_1_eventually_red) { return q->l1 == RED; }

/* Events for the first light */
EVENT(light_0_green)  { if (q->l0 == RED   && q->l1 == RED) { q->l0_prev = q->l0; q->l0 = GREEN; } }
EVENT(light_0_orange) { if (q->l0 == GREEN && q->l1 == RED) { q->l0_prev = q->l0; q->l0 = ORANGE; } }
EVENT(light_0_red)    { if (q->l0 == ORANGE)                { q->l0_prev = q->l0; q->l0 = RED; } }

/* Events for the second light */
EVENT(light_1_green)  { if (q->l1 == RED   && q->l0 == RED) { q->l1_prev = q->l1; q->l1 = GREEN; } }
EVENT(light_1_orange) { if (q->l1 == GREEN && q->l0 == RED) { q->l1_prev = q->l1; q->l1 = ORANGE; } }
EVENT(light_1_red)    { if (q->l1 == ORANGE)                { q->l1_prev = q->l1; q->l1 = RED; } }

/* Check other paths */

FROM(light_l0_red) { q->l0_prev = ORANGE; q->l0 = RED; } TO(light_l0_green) { return q->l0 == GREEN; }
FROM(light_l1_red) { q->l1_prev = ORANGE; q->l1 = RED; } TO(light_l1_green) { return q->l1 == GREEN; }

FROM(light_l0_green) { q->l0_prev = RED; q->l0 = GREEN; } TO(light_l1_green_2) { return q->l1 == GREEN; }
FROM(light_l1_green) { q->l1_prev = RED; q->l1 = GREEN; } TO(light_l0_green_2) { return q->l0 == GREEN; }

It shall still be valid:

=======================================
model     : demo.c
---------------------------------------
invariants: 3
goals     : 4
events    : 6
paths     : 4
=======================================
Paths from the initial state
states    : 5
=======================================
Path from light_l0_red
states    : 5
=======================================
Path from light_l1_red
states    : 5
=======================================
Path from light_l0_green
states    : 5
=======================================
Path from light_l1_green
states    : 5
=======================================
Info: All invariants are satisfied in all reachable states.
Info: Each goal is satisfied in at least one reachable state.
Info: All paths have been successfully explored.

License

This file is part of Belenos.

Belenos is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

Belenos is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with Belenos.  If not, see <https://www.gnu.org/licenses/>.

For further information about Belenos you can visit
https://codeberg.org/cdsoft/belenos