Check if AGREE contracts imply a cycle without pre (algebraic loop)

[cong-liu-2000]

In the following example, System "Counter" has a contract which enforces the current value of output "output" depend on the current value of input "count_up". While in System "UpDownFeedback", a contract enforces the current value of output "count_up" depend on the current value of input "val". "val" is directly connected with "output". This creates a cycle without delay (pre), or algebraic loop. The analysis of such kind of model in general is undecidable [1]. Maybe we should forbid algebraic loops.

1. N. Halbwachs, P. Caspi, P. Raymond and D. Pilaud, "The synchronous data flow programming language LUSTRE," in Proceedings of the IEEE, vol. 79, no. 9, pp. 1305-1320, Sept. 1991, doi: 10.1109/5.97300.

   package AgreeTiming public with Base_Types;

   annex agree{ const count_bound : Base_Types::Integer = 2; };

   system Controller features manual_reset : in event data port Base_Types::Integer; ctrl_reset : out event data port Base_Types::Integer; annex agree { guarantee "Controller event response" : event(ctrl_reset) = if ((-count_bound < manual_reset) and (manual_reset < count_bound)) then event(manual_reset) else false;
   guarantee "Controller value response" : ctrl_reset = manual_reset;
   }; end Controller;

   system Counter features ctrl_reset : in event data port Base_Types::Integer; run : in data port Base_Types::Boolean; count_up : in data port Base_Types::Boolean; output : out event data port Base_Types::Integer; annex agree { guarantee "Counter event response" : event(output) = (true -> (output != pre(output))); guarantee "Counter value response" : output = if event(ctrl_reset) then ctrl_reset else 0 -> (pre(output) + (if run then (if count_up then 1 else -1) else 0));
   }; end Counter;

   system UpDownFeedback features val : in event data port Base_Types::Integer; count_up : out data port Base_Types::Boolean; annex agree { guarantee "Count bounded up or down" : count_up = if (val >= count_bound) then false else if (val <= -count_bound) then true else (true -> pre(count_up)); }; end UpDownFeedback;

   system Top_Level features run : in data port Base_Types::Boolean; reset : in event data port Base_Types::Integer; output : out event data port Base_Types::Integer; annex agree { guarantee "Counts bounded" : (-count_bound < output) and (output < count_bound); guarantee "Relaxed counts bounded" : (-count_bound <= output) and (output <= count_bound); }; end Top_Level;

   system implementation Top_Level.impl subcomponents controller : system Controller; counter : system Counter; feedback : system UpDownFeedback; connections reset_in : port reset -> controller.manual_reset; reset_ctrl : port controller.ctrl_reset -> counter.ctrl_reset; count_out : port counter.output -> output; count_fb : port counter.output -> feedback.val; up_down : port feedback.count_up -> counter.count_up; run_in : port run -> counter.run; end Top_Level.impl;

end AgreeTiming;

[kfhoech]

The characterization of this model as having an algebraic loop is not correct. While if it were directly coded as a Lustre model this would be true, it is not true of interactions between system components modeled in AGREE. In AGREE the contracts are rendered applying PLTL into verification conditions which may be cyclic. Note that it is important that AGREE supports such circular verification conditions as many real-world systems have such interactions. However, the codification into Lustre by checking whether the inputs, outputs, and state of the model satisfy the logical contracts. This avoids the circularity.

Please see Compositional verification of architectural models D. Cofer, A. Gacek, S. Miller, M. Whalen, B. LaValley, L. Sha and Your "what" is my "how": iteration and hierarchy in system design M. Whalen, A. Gacek, D. Cofer, A. Murugesan, M. Heimdahl, S. Rayadurgam for a more detailed discussion.

Also, please examine the translation of this AADL/AGREE into Lustre to see this in action:

type Base_Types__Boolean = bool;
type Base_Types__Unsigned = int;
type Base_Types__Unsigned_64 = int;
type Base_Types__Unsigned_32 = int;
type Base_Types__Unsigned_16 = int;
type Base_Types__Unsigned_8 = int;
type Base_Types__Integer = int;
type Base_Types__Integer_64 = int;
type Base_Types__Integer_32 = int;
type Base_Types__Integer_16 = int;
type Base_Types__Integer_8 = int;
type Base_Types__Float = real;
type Base_Types__Float_32 = real;
type Base_Types__Float_64 = real;

node _TOP__controller(
  __ASSUME__HIST : bool;
  manual_reset___EVENT_ : bool;
  manual_reset : int;
  time : real;
  ctrl_reset___EVENT_ : bool;
  ctrl_reset : int
) returns (
  __ASSERT : bool
);
var
  __GUARANTEE0 : bool;
  __GUARANTEE1 : bool;
let
  __GUARANTEE0 = (ctrl_reset___EVENT_ = (if (((-2) < manual_reset) and (manual_reset < 2)) then manual_reset___EVENT_ else false));

  __GUARANTEE1 = (ctrl_reset = manual_reset);

  __ASSERT = (__ASSUME__HIST => (__GUARANTEE1 and __GUARANTEE0));

  --%IVC __GUARANTEE0, __GUARANTEE1;

tel;

node _TOP__counter(
  __ASSUME__HIST : bool;
  run : bool;
  count_up : bool;
  ctrl_reset___EVENT_ : bool;
  ctrl_reset : int;
  time : real;
  output___EVENT_ : bool;
  output : int
) returns (
  __ASSERT : bool
);
var
  __GUARANTEE0 : bool;
  __GUARANTEE1 : bool;
let
  __GUARANTEE0 = (output___EVENT_ = (true -> (output <> (pre output))));

  __GUARANTEE1 = (output = (if ctrl_reset___EVENT_ then ctrl_reset else (0 -> ((pre output) + (if run then (if count_up then 1 else (-1)) else 0)))));

  __ASSERT = (__ASSUME__HIST => (__GUARANTEE1 and __GUARANTEE0));

  --%IVC __GUARANTEE0, __GUARANTEE1;

tel;

node _TOP__feedback(
  __ASSUME__HIST : bool;
  val___EVENT_ : bool;
  val : int;
  time : real;
  count_up : bool
) returns (
  __ASSERT : bool
);
var
  __GUARANTEE0 : bool;
let
  __GUARANTEE0 = (count_up = (if (val >= 2) then false else (if (val <= (-2)) then true else (true -> (pre count_up)))));

  __ASSERT = (__ASSUME__HIST => __GUARANTEE0);

  --%IVC __GUARANTEE0;

tel;

node main(
  controller__ctrl_reset___EVENT_ : bool;
  controller__ctrl_reset : int;
  controller____ASSUME__HIST : bool;
  counter__output___EVENT_ : bool;
  counter__output : int;
  counter____ASSUME__HIST : bool;
  feedback__count_up : bool;
  feedback____ASSUME__HIST : bool;
  output___EVENT_ : bool;
  output : int;
  controller__manual_reset___EVENT_ : bool;
  controller__manual_reset : int;
  controller__time : real;
  counter__run : bool;
  counter__count_up : bool;
  counter__ctrl_reset___EVENT_ : bool;
  counter__ctrl_reset : int;
  counter__time : real;
  feedback__val___EVENT_ : bool;
  feedback__val : int;
  feedback__time : real;
  run : bool;
  reset___EVENT_ : bool;
  reset : int;
  time : real
) returns (

);
var
  __ASSUME__HIST : bool;
  __GUARANTEE0 : bool;
  __GUARANTEE1 : bool;
let
  --%MAIN;
  __ASSUME__HIST = (feedback____ASSUME__HIST and (counter____ASSUME__HIST and (controller____ASSUME__HIST and true)));

  __GUARANTEE0 = (((-2) < output) and (output < 2));

  __GUARANTEE1 = (((-2) <= output) and (output <= 2));

  assert (time = controller__time);

  assert _TOP__controller(controller____ASSUME__HIST, controller__manual_reset___EVENT_, controller__manual_reset, controller__time, controller__ctrl_reset___EVENT_, controller__ctrl_reset);

  assert (controller____ASSUME__HIST = __HIST(true));

  assert (time = counter__time);

  assert _TOP__counter(counter____ASSUME__HIST, counter__run, counter__count_up, counter__ctrl_reset___EVENT_, counter__ctrl_reset, counter__time, counter__output___EVENT_, counter__output);

  assert (counter____ASSUME__HIST = __HIST(true));

  assert (time = feedback__time);

  assert _TOP__feedback(feedback____ASSUME__HIST, feedback__val___EVENT_, feedback__val, feedback__time, feedback__count_up);

  assert (feedback____ASSUME__HIST = __HIST(true));

  assert (run = counter__run);

  assert (reset = controller__manual_reset);

  assert (reset___EVENT_ = controller__manual_reset___EVENT_);

  assert (controller__ctrl_reset = counter__ctrl_reset);

  assert (controller__ctrl_reset___EVENT_ = counter__ctrl_reset___EVENT_);

  assert (counter__output = output);

  assert (counter__output___EVENT_ = output___EVENT_);

  assert (counter__output = feedback__val);

  assert (counter__output___EVENT_ = feedback__val___EVENT_);

  assert (feedback__count_up = counter__count_up);

  assert true;

  assert (((time = 0.0) -> (time > (pre time))) and (true -> (time = ((pre time) + (time - (pre time))))));

  --%PROPERTY __ASSUME__HIST;
  --%PROPERTY __GUARANTEE0;
  --%PROPERTY __GUARANTEE1;

tel;

node __HIST(
  input : bool
) returns (
  hist : bool
);
let
  hist = (input -> ((pre hist) and input));

tel;

node __MinPos(
  a : real;
  b : real
) returns (
  ret : real
);
let
  ret = (if (a <= 0.0) then b else (if (b <= 0.0) then a else (if (a <= b) then a else b)));

tel;

node __Rise(
  input : bool
) returns (
  output : bool
);
let
  output = (input -> ((pre (not input)) and input));

tel;

node __Fall(
  input : bool
) returns (
  output : bool
);
let
  output = ((not input) -> ((pre input) and (not input)));

tel;

Also note that AGREE does contain an algebraic loop detection where relevant for application within the contract of each AADL Component Classifier.