Intent
Repeat the mission miss every m time units.
Template
PCTL
$
\mapping(\lit{repeat}\ \term{miss}\ \lit{every}\ \terminal{m} )=
\mapping(\term{miss})\wedge
\LTLg^{[0,\infty]}
(
\mapping(\term{miss}) \rightarrow
(
\LTLg^{[1,m-1]}(\neg\mapping(\term{miss}))
\wedge
(\LTLf^{[m,m]} (\mapping(\term{miss}))))
)
$
Variations
Examples and Known Uses
“perform inorder:
- Service A and C each for 2 timeunits within [0,8], and
- within [0, 7], service B for 3 time units and service C for 2 time units within [1,5], and
- Service A for 2 timeunits within [2, 6] or service C for 2 time units within [1,5], all repeatedly.”
Relationships
See the Pause, End and Timeout-Deadline patterns.