FSM-Oracle Release

Hoping this blogpost finds you all well and without any further ado, we’d like to announce a very important release for Statebox: the finite state machine oracle.

A considerable amount of time has been spent on both research (more amazing stuff about this will follow in the coming months) and on formalizing a formally verified version of our core in Idris, which in turn has been implemented by many people from our team (mainly Sjoerd, Alex and Andre, which I thank for the incredible work!).

What does it do?

Now that we have a version of the core released, I’d like to explain what it does. The idea is simple: You pass it a specification for a finite state machine/Petri net, an initial state and a sequence of actions, and the core will tell you if that sequence of actions is valid.

I know what you are thinking: “Wait what? You spent more than a year to get this?!” The short answer is “Yes, we have.” The long answer is “We decided to make an investment, and spent a lot of time developing our basic infrastructure so that building incrementally on it would be much easier later on”. An even better answer is: “Try it out yourself!”. In any case, with this post, I hope to convince you this choice is not as abysmally dumb as it sounds, but quite the opposite.

Typedefs and Typed Core

Several years ago we started two big projects at Statebox, namely Typedefs and Typed Core. Typedefs is a formally verified programming language for types and terms. Essentially, it allows to specify a universal format for types that can be recursively built out of type variables, products, coproducts and fixed point operators, and for their terms. Given Typedefs and their terms, one is able to automatically serialize and deserialize them to various formats, such as binary, S-expressions and JSON. This allows for a formally well-defined way of exchanging data between different programming languages.

On the other hand, typed core is a formally verified implementation of the main engine that tells us if a given sequence of transitions fired in a Petri net is valid or not. This is done in Idris, and relies on idris-ct, our formally verified category theory library.

Getting these two projects up to a point where they could be useful has been a lot of work, but it pays off! Now, we can just define our categories effortlessly using idris-ct, and import/export their signatures and morphisms using Typedefs.

This is exactly what we did in our first version of the core, which we completed roughly a month ago. In it, the user is able to feed the core with a specification for a finite state machine, an initial state and a sequence of actions, specified as a path in the underlying FSM graph. This specification is exchanged using JSON, as in the following example:

{
  "_0": {
    "_0": 5,
    "_1": [
      {
       "input": 1,
       "output": 1
      },
      {
       "input": 3,
       "output": 4
      },
      {
       "input": 2,
       "output": 1
      },
      {
       "input": 3,
       "output": 2
      }]
  },
  "_1": 3,
  "_2": [3, 2, 0]
}

Here, the first field specifies the “shape” of the FSM:

"_0": 5,
    "_1": [
      {
       "input": 1,
       "output": 1
      },
      {
       "input": 3,
       "output": 4
      },
      {
       "input": 2,
       "output": 1
      },
      {
       "input": 3,
       "output": 2
      }]

The first field tells us that the FSM has five vertexes, indexed 0, 1, 2, 3, 4 . The second field specifies the edges, indexed 0,1,2,3: The first edge goes from 1 to 1 , the second from 3 to 4 , the third from 2 to 1, the fourth from 3 to 2. All in all, the FSM looks like this:

Then we have:

  "_1": 3,
  "_2": [3, 2, 0]

Here the first field specifies the initial state (start from vertex 3), while the second one specifies a path, in this case (go through edge 3, then through edge 2, then through 0 ). The path is the one displayed below:

The point is that this JSON format is not arbitrary; it is the encoding of a Typedefs term. So if the term is malformed for whatever reason, Typedefs will throw an error automatically. We do not have to worry anymore about our parser being correct, because it is generated automatically from our definition!

Internally, a correct FSM specification is used as the signature to build the free category associated to it. Then, the path is evaluated: Either it forms a valid morphism or it doesn’t. If it doesn’t then we throw an error, if it does we check that the domain of such morphism is indeed the initial state specified. If this is the case we return a positive answer. In any case, the answer is again returned as a Typedefs term, and as such can be easily exchanged around.

All in all, our software works like an oracle. The cool thing is that we can be very flexible about the types we use to exchange computational objects around since TDefs will take care of serialization and parsing for us. Moreover, we are using categorical constructions as typecheckers, and not some ad-hoc thing.

The advantages of this approach are considerable. Less than two weeks ago we started working on the Petri net version of this, which amounts to taking symmetric strict monoidal categories as our typecheckers. We had already implemented those in idris-ct, and hence we were able to finish our work almost instantly. With an amount of minimal tweaking, we were able to recast our infrastructure completely to deal with Petri nets. Indeed, we are now in the process of documenting the new version of the core, which we will likely release in the coming months.

I hope that the advantages of employing categorical methods are now clear. It’s a lot of hassle in the beginning, but then things become way easier since in category theory everything is defined “canonically”, meaning that there is often just one way to do things, which is also the right one if you worked on the foundations of your project well enough.

Feel free to play with the oracle we released, and stay tuned for the new version that we’ll release soon!