This package exports a set of macros to synthesize static procedure-based automata from a declarative description of states, triggers and transitions with all states, triggers and transitions known at compile-time.
It is fast, composable, threadsafe, generates compact code and does not allocate on the heap.
Within each states you also have the full power of the Nim language instead of being restricted to only operations supported by a custom domain-specific language.
The generated state machine is a procedure, with parameters of your choosing that access in your states. You can easily call other procedures to build nested state machines or introduce a stack of past states to create a pushdown automata (for parsing Brainfuck or JSON for example).
A detailed usage tutorial is available at examples/water_phase_transitions.nim. It is executable.
This is a support library for the Weave multithreading runtime. Requirements for a multithreading runtime makes Synthesis also an excellent fit to generate state machines for embedded devices, protocols and managing complex event-driven workloads in general.
Here are 2 simple examples of the usage of Synthesis in production code to implement components of the Weave multithreading runtime.
This is the description of the transitions of a worker thread that ran out of tasks in its own task queue and checks if it managed to steal tasks from other threads. (The theft is handled in another state machine.)
type
RecvTaskState = enum
RT_CheckChannel
RT_FoundTask
RT_Event = enum
RTE_CheckedAllChannels
RTE_FoundTask
RTE_isWaiting
This is the description of the transitions of any thread that syncs (awaits) a future that may be handled in another thread.
In summary, while the awaited task has child tasks still pending in this worker thread, those are processed in priority, otherwise, it steals tasks from other threads to help them on their workload. As soon as the future is ready, it exits.
type AwaitState = enum
AW_CheckTask
AW_OutOfChildTasks
AW_Steal
AW_SuccessfulTheft
type AwaitEvent = enum
AWE_FutureReady
AWE_HasChildTask
AWE_ReceivedTask
The example below gives you a short overview of how to build your state machine.
Recipe:
- A state enum (called
Phasein the example) - An event/trigger/condition enum (called
Event) - Declaring a state machine
- Declaring prologue, epilogue, initial state, terminal state. SOme are optional
- Implement your events. Those are boolean tests.
Events have visibility on variables declared
- in the prologue
- in
onEntry - and the synthesized function parameters (here
tempFeed).synthesize(waterMachine): proc observeWater(tempFeed: var seq[float])
- Implement common setup and teardown on state entry and exit if needed
- Describe behaviours (i.e. state to state transition):
- Transition without condition
- Conditional transition due to an event
- "Interrupt" which is a conditional transition that shortcuts regular control flow
and allow handling exceptional cases, for example reaching the end of the
tempFeedsequence.
- Synthesize the state machine
- Run it
- ...
- Profit!
type Phase = enum
## States of your automaton.
## The terminal state does not need to be defined
Solid
Liquid
Gas
# Plasma is unused. On the graph display, it will not be reachable from the InitialState.
# The graph will also show that transitions out of the Plasma state are undefined via an `unreachable` transition.
Plasma
type Event = enum
## Named events. They will be associated with a boolean expression.
Over100
Between0and100
Below0
OutOfWater
# Common configuration
# -------------------------------------------
# Create a "waterMachine" entry.
declareAutomaton(waterMachine, Phase, Event)
# Optionally setup the "prologue". Extra state goes there, the variables are visible by all.
setPrologue(waterMachine):
echo "Welcome to the Steamy machine version 2000!\n"
var temp: float64
# Mandatory initial state. This must be one of the valid state of the state enum ("Phase" in our case)
setInitialState(waterMachine, Liquid)
# Terminal state is mandatory. It's a pseudo state and does not have to be part of the state enum.
setTerminalState(waterMachine, Exit)
# Optionally setup the "epilogue". Cleaning up what was setup in the prologue goes there.
setEpilogue(waterMachine):
echo "Now I need some coffee."
# Events
# -------------------------------------------
implEvent(waterMachine, OutOfWater):
tempFeed.len == 0
implEvent(waterMachine, Between0and100):
0 < temp and temp < 100
implEvent(waterMachine, Below0):
temp < 0
implEvent(waterMachine, Over100):
100 < temp
# `onEntry` and `onExit` hooks
# -------------------------------------------
#
# Those are applied on each state entry, before conditions are checked
# and on each state exits. The only exceptions are "interrupt" behaviours.
onEntry(waterMachine, [Solid, Liquid, Gas]):
let oldTemp = temp
temp = tempFeed.pop()
echo "Temperature: ", temp
# `behaviors`
# -------------------------------------------
#
# Interrupts are special triggers which ignores onEntry/onExit
#
# They allow the normal operations to make assumptions like
# a container not being empty or a value being available.
#
# They are also suitable to handle termination signals.
behavior(waterMachine):
ini: [Solid, Liquid, Gas, Plasma]
fin: Exit
interrupt: OutOfWater
transition:
echo "Running out of steam ..."
# Conditional state change, depending on temperature.
behavior(waterMachine):
ini: Solid
fin: Liquid
event: Between0and100
transition:
assert 0 <= temp and temp <= 100
echo "Ice is melting into Water.\n"
behavior(waterMachine):
ini: Liquid
fin: Gas
event: Over100
transition:
assert temp >= 100
echo "Water is vaporizing into Vapor.\n"
#...
# Steady state, if no phase change was triggered, we stay in our current phase
behavior(waterMachine):
steady: [Solid, Liquid, Gas]
transition:
# Note how we use the oldTemp that was declared in `onEntry`
echo "Changing temperature from ", oldTemp, " to ", temp, " didn't change phase. How exciting!\n"
# `Synthesize`
# -------------------------------------------
# Synthesizing the automaton will transform the previous specification
# into a concrete procedure with a name, type and inputs of your choosing.
#
# Assertions are inserted to ensure the automaton
# stops if a state+event combination was not handled.
#
# You can pass "-d:debugSynthesis" to view the state machine generated
# at compile-time.
#
# The generated code can also be copy-pasted for debugging or for further refining.
synthesize(waterMachine):
proc observeWater(tempFeed: var seq[float])
# Running the machine
# -------------------------------------------
import random, sequtils
echo "\n"
# Create 20 random temperature observations.
var obs = newSeqWith(20, rand(-50.0..150.0))
echo obs
echo "\n"
observeWater(obs)
# Output
# -------------------------------------------
# @[-3.460770047808822, 114.5693402308219, 16.66758940395412, 147.8992369379481, 38.74529893378966, -34.83679531473696, 68.73127270016445, -10.89306136942781, 55.17781700115015, 114.8825749296374, 86.88038583504948, 47.98729291960338, -40.94605405014646, 141.4807806383724, -19.78255259056119, -1.654260475969281, 37.0554825533913, 80.74588296425821, -7.707680239048244, 37.63170603752019]
# Welcome to the Steamy machine version 2000!
#
# Temperature: 37.63170603752019
# Changing temperature from 0.0 to 37.63170603752019 didn't change phase. How exciting!
#
# Temperature: -7.707680239048244
# Water is freezing into Ice.
#
# Temperature: 80.74588296425821
# Ice is melting into Water.
#
# Temperature: 37.0554825533913
# Changing temperature from 80.74588296425821 to 37.0554825533913 didn't change phase. How exciting!
#
# Temperature: -1.654260475969281
# Water is freezing into Ice.
#
# Temperature: -19.78255259056119
# Changing temperature from -1.654260475969281 to -19.78255259056119 didn't change phase. How exciting!
#
# Temperature: 141.4807806383724
# Ice is sublimating into Vapor.
# ...It is possible to display the finite state machine using Graphviz.
Synthesis representation can be converted to Graphviz ".dot" (or ".gv") with toGraphviz
Using the previous waterMachine
const dotRepr = toGraphviz(waterMachine)
writeFile("water_phase_transitions.dot", dotRepr)Note: The conversion is done at compile-time and stored in a string.
To convert the graph described in the graphviz file to a .png use the following command (assuming a shell and graphviz package being installed)
dot -Tpng water_phase_transitions.dot -o water_phase_transitions.pngFor SVG
dot -Tsvg water_phase_transitions.dot -o water_phase_transitions.svgA default style is used to differentiate between states, interrupts (exceptional events) and regular events/triggers.
Output of the waterMachine
Alternatives to Graphviz can be used on the .dot files if the output is unsatisfactory. Remember that graph node placement is usually an NP-complete task and requires heuristics to be solved that may not be optimal for your specific graph.
In that case consider splitting your finite state machine hence building hierarchical state machines.
The state machine is used as the core of a multithreading runtime:
-
Threading friendly:
- No GC or memory management on the heap
-
Visual debugging via printing the graph to ensure that all events are handled and no state leads to an unreachable code path.
-
Easy to map to model checking and formal verification via clearly labeled: states, events, transitions.
Multithreading is complex and the more we can prove properties (like the absence of deadlocks or livelocks) the more confidence we can have in the runtime.
-
Extremely fast and very low CPU-overhead, as overhead in the state machine means more latency in scheduling work. Furthermore, slowness effects are "scaled" by the number of cores.
-
Extensibility: as runtime requirements grow (distributed clusters, heterogeneous computing, fine-grained barriers, IO, continuations, cancellations,...),
Synthesis should help minimizing the potential for entangled control-flow and missing edge-cases.
Synthesis generates a procedure-based automaton using gotos for transitions:
- This avoids function calls/returns and associated pushing/poping stack overhead
- and switch dispatch branch prediction miss due to having a single point of dispatch..
In addition to the multithreading runtime requirements this architecture allow Synthesis to produce code with a very low footprint which makes it suitable for embedded. Furthermore, setPrologue/setEpilogue/onEntry/onExit and the transitions are very flexible, they can use inline statements, declare new variables or defer computation to one or more procs.
- Mealy State Machine
- Pushdown Automaton
- Communicating Finite State Machines
- Petri Nets
- Kahn Process Networks
Extras