diff --git a/examples/pdtmc/brp/brp.pm b/examples/pdtmc/brp/brp.pm index 897f9909e..7a3cb325b 100644 --- a/examples/pdtmc/brp/brp.pm +++ b/examples/pdtmc/brp/brp.pm @@ -133,3 +133,4 @@ module channelL [TO_Ack] (l=2) -> (l'=0); endmodule + diff --git a/examples/pdtmc/brp/brp16_2.pm b/examples/pdtmc/brp/brp16_2.pm index 2e20b7de4..0fc99d05e 100644 --- a/examples/pdtmc/brp/brp16_2.pm +++ b/examples/pdtmc/brp/brp16_2.pm @@ -133,3 +133,5 @@ module channelL [TO_Ack] (l=2) -> (l'=0); endmodule + +label "error" = s=5; diff --git a/examples/pdtmc/brp_rewards2/brp_rewards16_2.pm b/examples/pdtmc/brp_rewards2/brp_rewards16_2.pm index 0b05d22fd..7145a77ae 100644 --- a/examples/pdtmc/brp_rewards2/brp_rewards16_2.pm +++ b/examples/pdtmc/brp_rewards2/brp_rewards16_2.pm @@ -144,3 +144,5 @@ rewards endrewards +label "target" = s=5; + diff --git a/examples/pdtmc/brp_rewards4/brp_rewards16_2.pm b/examples/pdtmc/brp_rewards4/brp_rewards16_2.pm index d756a90ec..ff62fea14 100644 --- a/examples/pdtmc/brp_rewards4/brp_rewards16_2.pm +++ b/examples/pdtmc/brp_rewards4/brp_rewards16_2.pm @@ -144,3 +144,5 @@ rewards endrewards + +label "target" = s=5; \ No newline at end of file