Could someone please explain why the algorithm below prints <<Hello>> twice (unexpected), but when I comment out the assert at the end, it prints <<Hello>> only once (as expected)?
Thank you,
Yuri
EXTENDS Naturals, TLC
(*
--algorithm contraints
variable a = 0;
begin
L1: while a < 100 do
a := a + 1;
end while;
print <<"Hello">>;
assert FALSE;
end algorithm
*)