Problem description
As 762c382, every direction/initial set constraint and parameter constraint must be introduced by the reserved words direction and param. This is quite verbose and it may also be frustrating for the user.
Possible solution
A possible solution for the param word has been already proposed in #18.
As far as direction is concerned, we propose to support the following syntax:
directions_specification: "dirs" "=" "[" direction_list "]";
direction_list: | direction_list "," direction;
direction: linear_expression
where we assumed to decoupled the direction specification from the initial set specification (see #17).
This syntax, which resembles a Python list constructor, could also justify the successive adoption of dirs[i] as a shortcuts for the i-th specified direction.
For instance, a possible application of the proposed syntax could be:
problem: reachability;
iterations: 30;
var x, y;
dynamic(x) = x;
dynamic(y) = y + x*x*0.0001;
dirs = [x + y <=10, x>=0, y>=0];
assertion(dirs[0]<=20);
Problem description
As 762c382, every direction/initial set constraint and parameter constraint must be introduced by the reserved words
directionandparam. This is quite verbose and it may also be frustrating for the user.Possible solution
A possible solution for the
paramword has been already proposed in #18.As far as
directionis concerned, we propose to support the following syntax:where we assumed to decoupled the direction specification from the initial set specification (see #17).
This syntax, which resembles a Python list constructor, could also justify the successive adoption of
dirs[i]as a shortcuts for the i-th specified direction.For instance, a possible application of the proposed syntax could be: