Download Formal Refinement Support

D33.4 - Refinement Support (Public)
) ; X))
[| {sec} | {| ans, inc, minsReq |} | {min} |]
(mu X @ ((
inc ->
([frame wr min post min = (min
[]
minsReq -> ans!min -> Skip
) ; X))
)
) \\ {| ans, inc, minsReq |})
+ 1) mod 60])
(( ([frame wr min pre true post min = 0] ;
[frame wr sec pre true post sec = 0]) ;
((mu X @ ((
time -> minsReq -> ans?mins -> out!mins!sec -> Skip
[]
tick ->
([frame wr sec post sec = (sec + 1) mod 60]);(
[sec = 0]& inc -> Skip
[]
[sec <> 0]& Skip
)
) ; X))
[| {sec} | {| ans, inc, minsReq |} | {min} |]
(mu X @ ((
inc ->
([frame wr min post min = (min
[]
minsReq -> ans!min -> Skip
) ; X))
)
)\\ {| ans, inc, minsReq |})
+ 1) mod 60])
Now, we apply the law Sequential Composition Associativity 2
to the whole action except the hiding (\\{|...|}) in order to group the second
specification statement and the parallel action together.
(( [frame wr min pre true post min = 0] ;
([frame wr sec pre true post sec = 0] ;
21