-- specification AG (callstartwrite -> AF (callstartread1... is false
-- as demonstrated by the following execution sequence
state 1.1:
callwriteWork_def = 1
callstopwrite_def = 0
callstartwrite_def = 0
callstartread2_def = 1
callstartread1_def = 1
writerpresentfalse = 1
activereaders0 = 1
unchanged_except_writer__1 = 0
unchanged_except_read__write__control_wr... = 0
unchanged_except_read__write__control_re... = 0
unchanged_except_read__write__control_re... = 0
unchanged_except_read__write__control = 0
read__write__control_enabled = 1
reader__1_enabled = 0
reader__2_enabled = 0
writer__1_enabled = 1
Idle = 0
writer__1 = s1
callstartwrite = 0
callstopwrite = 0
callwriteWork = 0
reader__2 = s1
callstartread2 = 0
reader__1 = s1
callstartread1 = 0
read__write__control = s1

state 1.2:
read__write__control_enabled = 0
writer__1 = s2
callstartwrite = 1
read__write__control = s2

state 1.3:
read__write__control_enabled = 1
writer__1 = s3
callstartwrite = 0
callwriteWork = 1

-- loop starts here --
state 1.4:
reader__1_enabled = 1
reader__2_enabled = 1
writer__1 = s1
callstopwrite = 1
callwriteWork = 0
read__write__control = s3

state 1.5:
writerpresentfalse = 0
read__write__control_enabled = 0
reader__1_enabled = 0
reader__2_enabled = 0
writer__1 = s2
callstartwrite = 1
callstopwrite = 0
read__write__control = s10

state 1.6:
read__write__control_enabled = 1
writer__1 = s3
callstartwrite = 0
callwriteWork = 1

state 1.7:
writerpresentfalse = 1
reader__1_enabled = 1
reader__2_enabled = 1
writer__1 = s1
callstopwrite = 1
callwriteWork = 0
read__write__control = s3


resources used:
user time: 0.07 s, system time: 0.03 s
BDD nodes allocated: 4736
Bytes allocated: 917504
BDD nodes representing transition relation: 133 + 1