SIL initial set

[albertocasagrande]

Problem description

As 762c382, the initial set is provided as a set of constant constraints on the directions. This approach has three main drawbacks at least:

1. it misses to expose the initial set in the SIL syntax clearly;
2. it seems to force the users to specify one constraint per direction at least;
3. it does not support non-convex set specifications and limits the initial sets to be polytope-representable.

Possible solution

We suggest supporting an advanced initial set specification syntax such as the following one:

initial_set : "initial_set" "{" polytope_list "}";

polytope_list: | polytope_list "," polytope;

polytope: "{" constraint_list "}";

constraint_list: | constraint_list "," constraint

constraint: direction_identifier relation value 
              | direction_identifier "in" value_interval 
              | linear_expression relation linear_expression
              | linear_expression "in" value_interval;

relation: "=" | ">=" | "<=";

This syntax change will admit, for instance, the following SIL file:

problem: reachability;
iterations: 30;

var x, y;

dynamic(x) = x;
dynamic(y) = y + x*x*0.0001;

direction d_0: x + y;
direction x;
direction y;

initial_set {
  { d_0 <= 10, x >= 0, y>=0 },
  { d_0 <= 10, x >= y,  y in [0, 1] },
  { d_0 in [0,10], x-y in [0, 10]}
}