Network Automata DRH syntax

[danbryce]

We've developed a new syntax for drh files that includes some changes needed for networks of automata, but also some changes that are not specific to networks. I've included an example below. I'd like to integrate this syntax with dreal2 or dreal3, but am looking for input on how to proceed. We can update the existing benchmarks, use a different parser, merge the parsers, etc. Any suggestions?

Currently, we have a branch on bitbucket that is built off of dreal2 and modifies dReach only.

Here is the example:

[0, 100000] time;

(component train;
    [0, 5000] x;

    label approach, exit;

    (mode far;
        invt:
            (x >= 1000);
        flow:
            d/dt[x] = -1;
        jump:
            (approach): (x = 1000) ==> @near (true);
    )

    (mode near;
        invt:
            (x >= 0);
        flow:
            d/dt[x] = -1;
        jump:
            (): (true) ==> @past (x' = 0);
    )

    (mode past;
        invt:
            (x >= -100);
        flow:
            d/dt[x] = -1;
        jump:
            (exit): (x = -100) ==> @near (x' = 4900);
    )
)

(component gate;
    [0, 90] y;

    label raise, lower;

    (mode open;
        invt:
            (y <= 90);
        flow:
            d/dt[y] = 0;
        jump:
            (raise): (true) ==> @open (y' = y);
            (lower): (true) ==> @movedown (y' = y);
    )

    (mode closed;
        invt:
            (y = 0);
        flow:
            d/dt[y] = 0;
        jump:
            (lower): (true) ==> @closed (y' = y);
            (raise): (true) ==> @moveup (y' = y);
    )

    (mode movedown;
        invt:
            (y >= 0);
        flow:
            d/dt[y] = -9;
        jump:
            (): (true) ==> @closed (y' = 0);
            (lower): (true) ==> @movedown (y' = y);
            (raise): (true) ==> @moveup (y' = y);
    )

    (mode moveup;
        invt:
            (y >= 90);
        flow:
            d/dt[y] = 9;
        jump:
            (): (true) ==> @open (y' = 90);
            (raise): (true) ==> @moveup (y' = y);
            (lower): (true) ==> @movedown (y' = y);
    )
)

(component controller;
    [0, 100000] z;

    label lower, raise, approach, exit;

    (mode doup;
        invt:
            (z <= 5);
        flow:
            d/dt[z] = 1;
        jump:
            (exit): (true) ==> @doup (z' = z);
            (raise): (true) ==> @idle (z' = z);
            (approach): (true) ==> @dodown (z' = z);
    )

    (mode idle;
        invt:
        flow:
            d/dt[z] = 1;
        jump:
            (exit): (true) ==> @doup (z' = 0);
            (approach): (true) ==> @dodown (z' = 0);
    )

    (mode dodown;
        invt:
            (z <= 5);
        flow:
            d/dt[z] = 1;
        jump:
            (approach): (true) ==> @dodown (z' = z);
            (exit): (true) ==> @doup (z' = z);
            (lower): (true) ==> @idle (z' = z);
    )
)

analyze:
    train0 = train[[], @far (x=5000)];
    gate0 = gate[[], @open (y = 90)];
    controller0 = controller[[], @idle (z = 0)];
    (train0 || gate0 || controller0);

goal:
    (): (and (x <= 1000) (x >= 0) (y >= 0));
//  (): (and (x));

[kquine]

This looks good! If you are interested in, I have a few ideas that can also be applied to the networked hybrid system benchmarks. For the networked thermostat example, variables can be also shared; e.g., the thermostat 1 can use both temperature variables x1 and x2, while x2 is defined in the thermostat 2. Of course, we need to distinguish variable names, and x2 should be referenced as Thermo2.x2 in the component Thermo1. But we can also use a typical "use" command to define an alias. Here is some example (I also use a slightly different syntax that I think it is more clear):

#define c 0.01
#define gT 20
[0, 1] time;

component Timer
{
[0, 1] tau;
label step;

{mode tick;
    invt:   
        (tau >= 0);
        (tau <= 1);
    flow:
        d/dt[tau]  = 1;
    jump:
        [step]: (tau = 1) ==> @tick (tau' = 0);
}

init:
@tick (tau = 0);

}

component Thermo1
{
[-20, 100] x1;
[0.015] K1;
[100] h1;

use Thermo2.x2;    // x2 can be directly used in Thermo1
label step;

{mode on;
    invt:
    flow:
        d/dt[x1] = K1 * (h1 - ((1 - c) * x1 + c * x2));
    jump:
        [step]: (x1 <= gT) ==>  @on (x1’ = x1);
        [step]: (x1 > gT)  ==> @off (x1’ = x1);
}

{mode off;
    invt:
    flow:
        d/dt[x1] = K1 * (h1 - ((1 - c) * x1 + c * x2));
    jump:
        [step]: (x1 <= gT) ==>  @on (x1’ = x1);
        [step]: (x1 > gT)  ==> @off (x1’ = x1);
}

}

component Thermo2
{
[-20, 100] x2;
[0.045] K2;
[200] h2;

use xo = Thermo1.x1;   // variable renaming 
label step;

{mode on;
    invt:
    flow:
        d/dt[x2] = K2 * (h2 - ((1 - c) * x2 + c * xo));
    jump:
        [step]: (x2 <= gT) ==>  @on (x2’ = x2);
        [step]: (x2 > gT)  ==> @off (x2’ = x2);
}

{mode off;
    invt:
    flow:
        d/dt[x2] = K2 * (h2 - ((1 - c) * x2 + c * xo));
    jump:
        [step]: (x2 <= gT) ==>  @on (x2’ = x2);
        [step]: (x2 > gT)  ==> @off (x2’ = x2);
}

}

system:
(Timer || Thermo1 || Thermo2);

goal:
@(tick || ANY || ANY) (and (or (Thermo1.x1 < gT - 5) (Thermo1.x1 > gT + 5)) (or (Thermo2.x2 < gT - 5) (Thermo2.x2 > gT + 5)));