Type-safe finite state machines in zig!

I used to develop type-safe finite state machines in haskell.https://github.com/sdzx-1/typed-fsm

The same effect can be achieved by relying on some programming conventions in zig.

I made some examples using typed-fsm-zig: GitHub - sdzx-1/typed-fsm-zig: typed-fsm-zig

typed-fsm + gui is a very good choice!!!

7 Likes

The advantages described here also exist in zig!

Added more introduction!

5 Likes

The latest typed-fsm-zig simplifies the state and allows state transition functions based on state transition messages, which is a victory for abstraction.

code

6 Likes

Hello,

is there a way to have the GUI loop managed externally from the state machine logic?

From what I understand, your FSM can’t retain static typing unless genMsg runs the gui loop to retrieve the user input.
But, there are situations where the GUI can’t be run directly from genMsg(), for example if it’s managed by a host application.
I’ve looked into it, and I can’t find a solution: no matter what, if genMsg doesn’t own the loop, then you have to resort to using a dispatcher function, which nullifies the strong typing…

Any hints?

1 Like

This is really cool. Thanks for sharing.

I wonder if you’ve seen the CREM module?

IMO, it has some pretty interesting ideas that go a long way toward making illegal states materialize as type errors. It uses Singletons to do much of that. I wonder is that plausible or possible in Zig?

Another cool feature is being able to generate a diagram of all possible states and transitions solely using the code.

I don’t quite understand what you mean, are there any more specific examples.

I can’t fully understand this library yet, and I’m curious how it models uncertain states on type.

I redesigned the representation of the state machine on the type and allowed the existence of recursive types.

This is a huge improvement.

Here is an example of Atm, I can limit the number of checkPin times to not exceed 3 times. Actually I just need to implement a general handling function for checkPin state, and then I just need to express this constraint on the type. Then all interactions will be completed automatically, you will get an interface to input pins and try it up to 3 times.

code

    pub const readyST = union(enum) {
        InsertCard: EWitFn(.{ Atm.checkPin, Atm.session, .{ Atm.checkPin, Atm.session, .{ Atm.checkPin, Atm.session, Atm.ready } } }),
        Exit: EWit(.exit),

        pub fn handler(ist: *State) void {
            switch (genMsg(ist.window)) {
                .Exit => |wit| wit.handler(ist),
                .InsertCard => |wit| wit.handler(ist),
            }
        }
  .....
    pub fn checkPinST(success: typedFsm.sdzx(Atm), failed: typedFsm.sdzx(Atm)) type {
        return union(enum) {
            Successed: typedFsm.Witness(Atm, success, State, prinet_enter_state),
            Failed: typedFsm.Witness(Atm, failed, State, prinet_enter_state),

            pub fn handler(ist: *State) void {
                switch (genMsg(ist.window, &ist.pin)) {
                    .Successed => |wit| wit.handler(ist),
                    .Failed => |wit| wit.handler(ist),
                }
            }

            fn genMsg(window: *Window, pin: []const u8) @This() {
                var tmpPin: [4:0]u8 = .{ 0, 0, 0, 0 };
                while (true) {
                    init(window);
                    defer {
                        zgui.backend.draw();
                        window.swapBuffers();
                    }

                    {
                        _ = zgui.begin("CheckPin", .{ .flags = .{
                            .no_collapse = true,

                            .no_move = true,
                            .no_resize = true,
                        } });
                        defer zgui.end();

                        _ = zgui.inputText("pin", .{
                            .buf = &tmpPin,
                            .flags = .{ .password = true, .chars_decimal = true },
                        });

                        if (zgui.button("OK", .{})) {
                            for (0..4) |i| tmpPin[i] -|= 48;

                            if (std.mem.eql(u8, &tmpPin, pin)) {
                                return .Successed;
                            } else {
                                return .Failed;
                            }
                        }
                    }
                }
            }
        };
    }

It’s really interesting combination. Type combination brings the combination of front-end and back-end.

1 Like

A counter example

pub fn select_st(
    T: type,
    current_st: T,
    a: typedFsm.sdzx(T),
    b: typedFsm.sdzx(T),
    State: type,
) type {
    return union(enum) {
        SelectA: RWit(a),
        SelectB: RWit(b),
        Retry: RWit(typedFsm.sdzx(T).C(current_st, &.{ a, b })),

        fn RWit(val: typedFsm.sdzx(T)) type {
            return typedFsm.Witness(T, val, State, null);
        }

        pub fn handler(ist: *State) void {
            switch (genMsg()) {
                .SelectA => |wit| wit.handler(ist),
                .SelectB => |wit| wit.handler(ist),
                .Retry => |wit| wit.handler(ist),
            }
        }

        const stdIn = std.io.getStdIn().reader();
        var buf: [10]u8 = @splat(0);

        fn genMsg() @This() {
            std.debug.print(
                \\Input your select:
                \\y={}, n={}
                \\
            ,
                .{ a, b },
            );

            const st = stdIn.readUntilDelimiter(&buf, '\n') catch |err| {
                std.debug.print("Input error: {any}, retry\n", .{err});
                return .Retry;
            };

            if (std.mem.eql(u8, st, "y")) {
                return .SelectA;
            } else if (std.mem.eql(u8, st, "n")) {
                return .SelectB;
            } else {
                std.debug.print(
                    \\Error input: {s}
                    \\You cant input: y={}, n={}
                    \\
                , .{ st, a, b });
                return .Retry;
            }
        }
    };
}

Defining a simple universal select state can implement very complex logic and has good composability.

1 Like

I add some examples of using typed-fsm here.
vidoe