(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Parametric timed pattern matching benchmark: accel
 *
 * Description     : Parametric timed pattern matching benchmark: accel
 * Correctness     : N/A
 * Source          : Benchmarks for Temporal Logic Requirements for Automotive Systems (ARCH@CPSWeek 2014) + Masaki Waga / Étienne André, Ichiro Husuo, Masaki Waga "Offline timed pattern matching under uncertainty" (ICECCS 2018)
 * Author          : The same
 * Modeling        : Étienne André
 * Input by        : Étienne André
 * License         : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 *
 * Created         : 2020/08/18
 * Last modified   : 2021/02/08
 *
 * IMITATOR version: 3
 ************************************************************)


(************************************************************)
(* Property specification *)
(************************************************************)

property := #synth EF(loc[pta] = s_end);