urgent channels in XTA

[pascalpoizat]

Description

The urgent channels of XTA (see https://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf page 6) do not seem to be supported, at least in the XTA editor.

How to reproduce

Open file:

urgent chan sys_2_o2_res, sys_2_o2_req, sys_1_o1_req;

process sys_e() {

state
    l_error,
    l_correct,
    l_s0,
    l_s1,
    l_s2;
init l_s0;
trans
    l_s0 -> l_s1 { sync sys_1_o1_req!;  },
    l_s0 -> l_error { sync sys_2_o2_req!;  },
    l_s1 -> l_s2 { sync sys_2_o2_req!;  },
    l_s2 -> l_correct { sync sys_2_o2_res?;  },
    l_correct -> l_correct {  },
    l_error -> l_error {  };
}

process sys_s() {
clock c_6884493603270001633, c__3232429354967973480;
state
    l_sNEW {c_6884493603270001633 <= 4},
    l_s0,
    l_s1 {c_6884493603270001633 <= 4},
    l_s2 {c__3232429354967973480 <= 5},
    l_s3;
init l_s0;
trans
    l_s1 -> l_sNEW { guard c_6884493603270001633 >= 2;  },
    l_s0 -> l_s1 { sync sys_1_o1_req?; assign c_6884493603270001633 = 0;  },
    l_sNEW -> l_s2 { sync sys_2_o2_req?; assign c__3232429354967973480 = 0;  },
    l_s2 -> l_s3 { guard c__3232429354967973480 >= 2; sync sys_2_o2_res!;  },
    l_s3 -> l_s3 {  };
}
Process_sys_e = sys_e();
Process_sys_s = sys_s();
system Process_sys_e, Process_sys_s;

[yanntm]

no, urgent channels, as well as several other features (e.g. global clocks) are not in there.

But I can add them in if you need them.

[pascalpoizat]

Indeed I am still doing some experiments. Maybe I will be able to do with committed/urgent states rather than urgent channels.