You cannot select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
Timothy Bourke 4dadf6b4d6 Enforce well-formedness of clocks
For a clock (ck on x) to be well-formed in an environment H, we must
have H x = ck, i.e., the clock of x is the same as the clock ck of the
stream being sampled.

This constraint is guaranteed by construction for fully inferred clocks
(by the rules for when and merge), but nothing guarantees that user
declarations be well-formed. This can lead to problems.

For instance, this invalid program is incorrectly accepted:

    node f (x : bool; a : bool :: . on b;
		      b : bool :: . on a) returns (y:bool);
    let
	y = true;
    tel

as is this one:

    node f(a: bool :: . on a; b: bool :: . on a)
    returns (z: bool);
    var w : bool;
    let
	w = a when b;
	z = false fby w;
    tel

This invalid program is incorrectly accepted and leads to an internal
compiler error:

    node f (x : bool) returns (y:bool);
    var a : bool :: . on b;
	b : bool :: . on a;
    let
	y = true;
	a = true;
	b = true;
    tel

This patch enforces the well-formedness constraint. It gives a sensible
error message when the constraint cannot be satisfied.
7 years ago
..
analysis Enforce well-formedness of clocks 7 years ago
ctrln Adapt to new interface of reatk.ctrlNbac (≥ 0.11) 7 years ago
main Added simple scheduler with -simple-scheduler option 7 years ago
sigali Switch to non-deprecated String functions 7 years ago
transformations Added simple scheduler with -simple-scheduler option 7 years ago
_tags Upgrading to new ReaTK API (>= 0.9.4). 10 years ago
minils.ml Added syntax for reachability and attractivity in contracts 10 years ago
mls_compare.ml Added Marc as co-author 12 years ago
mls_mapfold.ml Added syntax for reachability and attractivity in contracts 10 years ago
mls_printer.ml Added syntax for reachability and attractivity in contracts 10 years ago
mls_utils.ml Fixed warnings. 10 years ago