When expression must be the argument of a current operator

[hbourbouh]

Hi Daniel,
How we can define a stream that is clocked in Kind2 syntax?
As it seems from the following code, Kind2 asking me to use the "current" operator when I use "when". In Lustre, we can define streams that are clocked by some bool clock.

node _make_clock(per: int; ph: int)
returns( clk: bool );
var cnt: int;
let
cnt = ((per - ph) -> (pre(cnt) + 1)) mod per ;
clk = if (cnt = 0) then true else false ;
tel
node trigger_test_PP(In1_1 : real;)
returns(Out1_1 : real;);
var RateTransition_1 : real;
RateTransition1_1 : real;
__time_step : real;
_clk_2_0 : bool ;
let
RateTransition_1 = (In1_1 when _clk_2_0);
RateTransition1_1 = (merge _clk_2_0
(true -> (0.000000000000000 -> (pre RateTransition_1)))
(false -> ((0.000000000000000 -> (pre RateTransition1_1)) when not(_clk_2_0))));
Out1_1 = RateTransition1_1;
__time_step = (0.0 -> ((pre __time_step) + 1.000000000000000));
_clk_2_0 = _make_clock(2, 0);
tel

Thanks,
Hamza

[daniel-larraz]

Hi Hamza,

Uses of the when operator alone are not legal in Kind2 (and Lustre) (see the "Merge, When, Activate and Restart" subsection in Kind 2 documentation). That restriction prevents RateTransition_1 from being undefined when _clk_2_0 is false. The error you are getting suggests the use of the current operator, which keeps the value of a stream between two steps, in combination with the when operator in order to avoid undefined values. This suggestion is unfortunate because the current operator is considered deprecated in the latest version of Kind 2, and it should have recommended the use of the merge operator instead. All in all, the key point is the when operator must be used in combination with other operators to avoid undefined values.

Best,
Daniel

[hbourbouh]

Hi Daniel,
Thanks for the reply.
The variable RateTransition_1 is used in a merge expression. It is a normalized expression.
Do you have a reference to the official documentation that explains why we can not create intermediate variables for a merge expression?
Best Regards,
Hamza

[daniel-larraz]

Hi Hamza,
If you want more information about combining streams on different rates you should take a look into:
"Clocks as First Class Abstract Types", J.-L. Colaço and M. Pouzet, 2003.
However, notice that Kind 2 does not implement a full clock calculus, and thus, the set of inputs that Kind 2 considers legal is more restricted than the one allowed by other Lustre compilers.
Cheers,
Daniel

[hbourbouh]

Hi Daniel,
To keep track of what we discussed, the following code is accepted by lv6 and not kind2.

node _make_clock(per: int; ph: int)
returns( clk: bool );
var cnt: int;
let
cnt = ((per - ph) -> (pre(cnt) + 1)) mod per ;
clk = if (cnt = 0) then true else false ;
tel
node trigger_test_PP(In1_1 : real;)
returns(Out1_1 : real;);
var --RateTransition_1 : real;
RateTransition1_1 : real;
__time_step : real;
_clk_2_0 : bool  ;
let
--RateTransition_1 = (In1_1 when _clk_2_0);
RateTransition1_1 = (merge _clk_2_0
(true -> (0.000000000000000 -> (pre (In1_1 when _clk_2_0))))
(false -> ((0.000000000000000 -> (pre RateTransition1_1)) when not(_clk_2_0))));
Out1_1 = RateTransition1_1;
__time_step = (0.0 -> ((pre __time_step) + 1.000000000000000));
_clk_2_0 = _make_clock(2, 0);
tel

[hbourbouh]

Hi Daniel,

In the same topic of the current issue, the following example is using Merge operator as you recommended. But I still get the same error above: " When expression must be the argument of a current operator".

node f (x: int ) returns (y: int);
let
 y = 0 -> x + pre y;
tel

node top (x:int) returns (o1,o2:int)
var c: bool;
let
c = true -> not pre c; --( x > 0 )
o1 = merge( c ; f(x) when c; 0 when not c);
o2 = merge( c ; f(x when c); 0 when not c);
tel

The above example is defining two streams: o1 and o2 wherein both function f is called at a different rate. Memories of function f will be updated at all-time in the case of "o1", whereas function f is only run when clock "c" is true in the case of "o2".