Recall that real-time response and liveness properties must be checked
by declaring the atomic properties using <#293#>sf<#293#> declarations in
<#294#>sample.sf<#294#>.
verbatim114#
The property S7 is thus invalid. The file <#297#>sample.output<#297#> contains
the failing legal trajectories.