HEADS-project / training

Training material to get started with the HEADS technologies
10 stars 16 forks source link

Does ThingML support non-determinism like in FSM theory #100

Closed FeltonXuAtECNU closed 8 years ago

FeltonXuAtECNU commented 8 years ago

state Init{ transition -> Init event timer?timer_timeout action do print "OutdoorTempSensor: send a value\n" sendPort!outdoorTemp(5) end transition -> BCD event timer?timer_timeout action do print "abc" // do some complex algorithm end }
Does this kind of non-determinism scenario could be modelled in ThingML? If could, what should I do?

brice-morin commented 8 years ago

It can, but will be non-derterministic at runtime. Our checker (currently being implemented will detect that). If you want both transition to be triggered, you should define a parallel region.

FeltonXuAtECNU commented 8 years ago

Also, a pretty easy one but can't find them on toy example. datatype Integer @c_type "int" @c_byte_size "2" @js_type "int" @java_type "int" @java_primitive "true";

How to write a datatype Double?

brice-morin commented 8 years ago

See https://github.com/SINTEF-9012/ThingML/blob/master/org.thingml.samples/src/main/thingml/datatypes.thingml

Basically define

datatype Double

And a the proper annotation(s) to map it to the concrete type for the platform you want to target

FeltonXuAtECNU commented 8 years ago

ThingML model is like this:

statechart HelloWorld init Greetings { 

    state Greetings { 

        transition -> Hi
        action print "Hi\n"

        transition -> Bye  
        action print "Hello World!\n" 

    } 

    state Bye { 
        on entry print "Bye.\n" 
    } 

    state Hi {
        on entry print "Hi ben!\n"
    }

} 

but I got something like this all the time, and that doesn't make sense for me: felton@ubuntu:~/Downloads/thingml-gen/posix/HelloCfg$ ./HelloCfg Hi Hi ben! ^C felton@ubuntu:~/Downloads/thingml-gen/posix/HelloCfg$ ./HelloCfg Hi Hi ben! ^C

So I posted the issues about non-determinism, so you don't have to close the issues so quickly.

brice-morin commented 8 years ago

It makes sense, your state machine is not deterministic. It appears that from Greetings the first transition will be triggered, going to the Hi state, hence producing sensible output:

Hi
Hi ben!

However, nothing prevents that sometimes, on some other platforms, the other transition could be fired.