boschresearch / blech

Blech is a language for developing reactive, real-time critical embedded software.
Apache License 2.0
72 stars 6 forks source link

Implementing state machine in blech #70

Closed MohamedGhardallou closed 5 days ago

MohamedGhardallou commented 2 years ago

Hello, When i tried to implement a state machine in blech i ended up with a code like this:

activity app()()
    var state : nat8 = 0
    var current_state : nat8 = 0
    var err_code : nat8 = 0

    when state != current_state then
        current_state = state
        if current_state == 0 then
            err_code = run activity_init()()
            if err_code != 0 then
                state = 4
                await true
            end
            state = 1
            await true
        elseif current_state == 1 then
            var err_code = run activity2()(output)
            if err_code != 0 then
                state = 4
                await true
            end
            if output == true then
                state = 2
                await true
            else
                state = 3
                await true
            end
        elseif current_state == 2 then
            run activity3()()
            state = 1
            await true
        elseif current_state == 3 then
            run activity4()()
            state = 1
            await true
        elseif current_state == 4 then  // error state
            run report_error()()
            state = 0
            await true
        end
        state = 0
        await true
        end
end

Can't we have a langage construct that we can use to implement state machines. It would be great also if "state changes" are instantaneous

activity app()()
    var err_code : nat8 = 0
    Switch(state : nat8)
        case 0:
            err_code = run activity_init()()
            if err_code != 0 then
                goto 4  // instantaneous jump to report_error. No need to wait for the next tick
            end
            goto 1
        case 1:
            var err_code = run activity2()(output)
                if err_code != 0 then
                    goto 4
                end
                if output == true then
                    goto 2
                    await true
                else
                    goto 3
                end
        case 2:
            run activity3()()
            goto 1
        case 3:
            run activity4()()
            goto 1
        case 4:
            run report_error()()
            goto 0
        default:
            goto 0
    end
end

This can make code a lot easier to read and to reason about. What do you think about this ? Thanks

schorg commented 2 years ago

In Blech, we offer control flow to implement state machines. We think that state machines quickly become too complicated if they grow. So your example could look like this

activity app () ()
    var err_code: nat8 = 0 
    repeat   
        err_code = run activity_init()()
        if err_code != 0 then
            run report_error()()
        else
            repeat
                var output: nat8 = 0
                err_code = run activity2()(output)
                if err_code != 0 then
                    run report_error()()
                elseif output == true then
                    run activity3()()
                else // output == false
                    run activity4()()
                end
            until err_code != 0 end
        end
    end
end

In words: First initialize everything then repeat doing activity2 followed activity3 or activity4 depending on the result. If something goes wrong, report the error and start over with initialization. By the way: activity3 and activity4 cannot terminate with an error.

schorg commented 2 years ago

One more thing. If report_error is a function - executed immediately, and does not contain await - you can use error_code to restart from the beginning by using when .. reset (https://www.blech-lang.org/docs/user-manual/statements/#abort-and-reset), but you need an additional await to not leave the when ... reset-block or repeat the inner loop, in case of an error:

activity app () ()
    var err_code: nat8 = 0 
    when err_code != 0 reset  
        err_code = run activity_init()()
        if err_code != 0 then
            report_error()
            await true
        else
            repeat
                var output: nat8 = 0
                err_code = run activity2()(output)
                if err_code != 0 then
                    report_error()
                    await true
                elseif output == true then
                    run activity3()()
                else // output == false
                    run activity4()()
                end
            end
        end
    end
end

But maybe, the following code with an error reporting function - instead of an activity - is the simplest:

activity app () ()
    repeat 
        var err_code: nat8 = 0 
        err_code = run activity_init()()
        if err_code != 0 then
            report_error()
        else
            repeat
                var output: nat8 = 0
                err_code = run activity2()(output)
                if err_code != 0 then
                    report_error()
                elseif output == true then
                    run activity3()()
                else // output == false
                    run activity4()()
                end
            until err_code != 0 end
        end
        await true
    end
end
MohamedGhardallou commented 2 years ago

Hi, Yes this example can be rewritten but i prefer to keep the state machine structure for readability. When you have more states and multiple transitions you can no longer rewrite it using "traditional approach" without loosing the "structure" of you problem.

I believe that supporting Statechart (which enable concurrent and hierarchical state machine) as a language construct can improve developer productivity and code readability ( and also address the state explosion problem ).

I think that Statechart can also be implemented with the current blech language features. For example in [1] without changing the main language, they added Statechart as a high order construct.

what do you think about this ?

[1] https://www.di.ens.fr/~pouzet/bib/emsoft05b.pdf

schorg commented 2 years ago

In order to keep an overview of the "structure" of your solution. We experimentally added a visualization of the hierarchical state/mode diagrams, that are expressed in the control flow of activities.

During development you can change your control flow and always get an up-to-date visualization.

There is a paper on this: https://ieeexplore.ieee.org/document/9568375 and a slide set, presented at a small workshop: http://synchron2021.inria.fr/slides/synchron2021-vonhanxleden.pdf

Currently it is not integrated into the Blech tools.

schorg commented 2 years ago

Maybe we should take the discussion to our Slack: https://join.slack.com/t/blech-lang/shared_invite/enQtODkyMDg4MDQ2Mjc2LWZjZWI1MmE2NTNhOGU0ZTVmMGEzMzY1ODlmNzBlMDFhMTIwMDRlZDA1MmU2NjY2OTFlZTA1NWIwMzU3NThkY2I

schorg commented 2 years ago

Some more hints from my side:

  1. Substituting state machines through control-flow of activities, was one of the motivations for Blech, being frustrated with state machines, which are often wrong, are not easy to refactor, constantly grow if changes are required, ...
  2. Lustre (in the emsoft paper) needs a way of specifying state machines, because Lustre originally does not have any imperative features, like control-flow, variables. General I think that state machines in a language are a DSL-thing which does not fit well to the orthogonality of languages features.
  3. When we started Blech, we also supported our colleague @mterber in his PhD-Thesis where he compares classical embedded programming to imperative synchronous programming: https://www.semanticscholar.org/paper/Real-world-deployment-and-evaluation-of-synchronous-Terber/0c0a9ce7b0831dee853bf488d45546f344c387dc . There is also a chapter where he compares software qualities of state-machine oriented programming to an imperative synchronous solution.
MohamedGhardallou commented 2 years ago

Thank you very much for the invitation and for the links. I will try to take a more deep look at this.