-title-not-set-

Nr	Name	Value
1	x	?
2	y	?

Nr	Name	Value
1	ANIMATION_EXPRESSION	?

Nr	Name	Enabled
1	Next	?

MACHINE Demo01_no_tlaps
ABSTRACT_VARIABLES
  x,
  y
/* PROMOTED OPERATIONS
  Next */
INITIALISATION
    x,y : (x = 0.0 & y = 1.0)
ACTIONS
  Next = 
    BEGIN
      x,y := (2.0 / 3.0) * x + 0.5 * y,0.5 * x - (1.0 / 3.0) * y
    END
/* DEFINITIONS
  PREDICATE Init;
  EXPRESSION ANIMATION_EXPRESSION;
  EXPRESSION VISB_JSON_FILE; */
END

Nr	Event	Target State ID
1	INITIALISATION(x=0.0,y=1.0)
2	Next
3	Next
4	Next
5	Next
6	Next
7	Next
8	Next
9	Next
10	Next
11	Next
12	Next
13	Next
14	Next
15	Next
16	Next
17	Next
18	Next
19	Next
20	Next
21	Next
22	Next
23	Next
24	Next

Generated on 2/5/2024 at 10:01 using ProB version 1.13.1-nightly
Main specification file: Demo01_no_tlaps.prob (modified on 1/5/2024 at 8:37)
Main specification name: Demo01_no_tlaps
Main VisB JSON file: Demo01_visb.json (modified on 1/5/2024 at 11:52)