Mirror of forum.nim-lang.org

5688 :: Introducing Synthesis: a Finite State Machine generator

• mratsim (orginal) [2019-12-14T22:45:14+01:00] view original

  While working on Project Picasso/Weave, I kept being lost in my own control flow and had the nagging impression that I should refactor the core to better handle the complexity.

  So I wrote a state machine generator. Hopefully just in time for people to use it in Advent of Code.

  It has the following features:

  • It generates a static state machine at compile-time, with supports from the Nim compiler to make sure you don't do bad things
  • It is multithreading friendly, in particular it doesn't allocate any heap memory (threadsafe memory handling compounds hard-to-debug memory bugs with hard-to-debug multithreading bugs, you don't want to go there).
  • It generates compact code: the code generator is based on the undocumented goto pragma. The states declared don't even exist in the generated code, only jumps remain, Super Mario-style.
  • It should generate among the fastest state machines.

    I'm no state machine optimization expert but anything based on transition tables will lose due to cache misses and anything based on switch dispatch will lose due to having a single point of dispatch (the switch) which will cause branch-prediction misses as soon as the states get numerous.

  • Events and transitions uses the full power of the Nim language, it is not restricted to a domain-specific language
  • It is procedure-based, with the procedures having a signature of your choosing. It is inherently side-effect free and no mutable state, contrary to object-oriented approaches.
  • It is composable
    • your state machine can easily call another state-machine and pass some parameters to build hierarchical state machines
    • the state machine can have any number of extra variables declared in its prologue, for example a stack.

      This in turn allow to generalize the FSM to a pushdown automata to parse your lovely Brainfuck or your boring JSON.

  • It is tested, given the use of an undocumented feature, better be ahead of the curve.
    • Travis: Linux, MacOS, x86_64 and ARM64
    • Appveyor: Windows 32-bit and 64-bit
    • Both on Nim stable and devel
  • The code behind is actually very simple and could be an good introduction to macros.

  Repo: https://github.com/mratsim/Synthesis

  For now I don't plan to expand the library more as it is fairly complete for my use case. The most interesting additions would be a graph backend and maybe saving/loading state machine definitions from JSON.

  Snippet

  type Phase = enum
    ## States of your automaton.
    ## The terminal state does not need to be defined
    Solid
    Liquid
    Gas
    Plasma # Plasma is almost unused
  
  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 obeservations.
  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.
  # ...
  Run

---

• geotre (orginal) [2019-12-17T18:44:01+01:00] view original

  Thanks @mratsim, this is really useful.

  For now I don't plan to expand the library more as it is fairly complete for my use case. The most interesting additions would be a graph backend and maybe saving/loading state machine definitions from JSON.

  What does graph backend mean in this case?

---

• Araq (orginal) [2019-12-18T09:44:40+01:00] view original

  It generates compact code: the code generator is based on the undocumented goto pragma.

  Maybe it's time to document it then... :-)

---

• mratsim (orginal) [2019-12-18T12:31:44+01:00] view original

  Something like Graphviz or GraphML to display the state machine with its transition visually.

---

• rayman22201 (orginal) [2019-12-18T22:15:24+01:00] view original

  @mratsim. You are awesome as always.

  Since the state machines can be nested, I wonder if this could be used to facilitate a heap free (and possibly stack free) async implementation, suitable for embedded.

  hrmm.... :-)

---

• mratsim (orginal) [2020-04-21T23:51:24+02:00] view original

  And Synthesis 0.2.0 is out, with the mentioned graph backend.

  Link to generating graphs: https://github.com/mratsim/Synthesis#displaying-the-state-machine

  And some graphs with increasing complexity

  Out-of-tasks worker state machine

  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
  Run

  sync (await) a task that may be spawned on another thread

  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
  Run

  @rayman22201 Yes it can facilitate both stack-free and heap-free implementation (states are "goto labels" at a low-level so they are not even represented by an enum or an integer. However for async the state machine would need some kind of context to know where to resume from.

---