summaryrefslogblamecommitdiff
path: root/tests/source/train.scade
blob: 0b93b2f2658697fe7cab483aa3ac7654257987d1 (plain) (tree)
1
2
3
4
5
6
7
8
9
10
11










                                               
                                                                                




                                   
                              
                                            

                   
                             
                                             



                             
                             
                                            

                  
                            
                                            








                                                      
                              
                                    

                   

                                           


                  
                                                                                   
   
                                             







                                                   
                                                                      
                               
                                                   

   
-- Cet exemple est clairement trop compliqué.


node diff(incr, decr: bool) returns (diff: int)
let
    diff = (0 -> pre diff) +
        (if incr and not decr then 1
        else if not incr and decr then -1
        else 0);
tel

node train(beacon, second: bool) returns (early, late: bool; probe advance: int)
let
    advance = diff(beacon, second);

    automaton
        initial state NotEarly
        let early = false; tel
        until if advance >= 10 resume Early;

        state Early
        let early = true; tel
        until if advance = 0 resume NotEarly;
    returns early;

    automaton
        initial state NotLate
        let late = false; tel
        until if advance <= -10 resume Late;

        state Late
        let late = true; tel
        until if advance = 0 resume NotLate;
    returns late;
tel

node observer(early, late: bool) returns (alarm: bool)
var ontime: bool;
let
    ontime = not (late or early);
    automaton
        initial state Ok
        let alarm = false; tel
        until if early resume Early;

        state Early
        let alarm = late and not early; tel
        until if ontime resume Ok;
    returns alarm;
tel

node train_check(beacon, second: bool) returns (early, late, alarm: bool; adv: int)
let
    early, late, adv = train(beacon, second);
    alarm = observer(early, late);
    guarantee ok : not alarm;
tel

node test(i: int) returns(a, b, c: int; exit: bool)
var early, late, alarm: bool;
let
    exit = i >= 100;
    early, late, alarm, a = train_check((i+1) mod 2 = 0, i mod 3 = 0);
    c = if alarm then 1 else 0;
    b = if early then 1 else if late then 2 else 0;
tel