only one prop file

benchmarks/benchmarks.sh

@@ -76,7 +76,7 @@ function run_benchmark {
   agents=$(cat ${model_folder}/${model}.imi | grep "^\s*automaton" | awk '{ print $2; }')
 
   # imitator files
-  prop_file="${model}-EFwitness.imiprop"
+  prop_file="EFwitness.imiprop"
   model_path="${model_folder}/${model}.imi"
 
   for a in $agents; do
@@ -84,7 +84,7 @@ function run_benchmark {
       echo -e "\nreaching $a @ $l"
 
       # 3) run imitator
-      new_prop_path="${output_folder}/${prop_file}.${l}"
+      new_prop_path="${output_folder}/${model}-${prop_file}.${l}"
       if [[ ! -f "${new_prop_path}.res" ]]; then
         sed "s/<replace>/loc[${a}] = ${l}/" "${model_folder}/${prop_file}" >"${new_prop_path}"
         echo "Running (timeout: ${timeout}) ${model} with ${new_prop_path}"

benchmarks/models/EFwitness.imiprop

+property := #witness EF(<replace>);
\ No newline at end of file

benchmarks/models/Pipeline_KP12_2_3-EFwitness.imiprop

-(************************************************************
- *                      IMITATOR MODEL
- *
- * Producer/Consumer with n=2 processing nodes of length m=3
- *
- * Description     : The network presented in Figure 2 models the system consisting of the Producer feeding the Consumer with data sent through a sequence of nodes with additional processing capabilities. The model is scalable with respect to the number n of the processing nodes and the length m of each processing node and it contains three lower (a,c,e) and three upper (b,d,f) parameters. Note: the clocks were renamed (w.r.t. to [KP12]) for sake of simplicity.
- * Correctness     : φ2 = ConsWaiting ∧ ProdReady ∧ xtotal ≥ 5
- * Source          : SMT-based Parameter Synthesis for L/U Automata, Michał Knapik and Wojciech Penczek
- * Author          : Michał Knapik and Wojciech Penczek
- * Modeling        : Michał Knapik and Wojciech Penczek
- * Input by        : Étienne André
- *
- * Created         : 2020/08/18
- * Last modified   : 2020/08/18
- *
- * IMITATOR version: 3
- ************************************************************)
-
-(************************************************************)
-(* Property specification *)
-(************************************************************)
-
-(* φ2 = ConsWaiting ∧ ProdReady ∧ xtotal ≥ 5 *)
-(* property := #witness EF(loc[Consumer] = consWaiting & loc[Producer] = prodReady (*& xtotal >= 5*) & loc[observer] = finished); *)
-
-property := #witness EF(loc[Pipeline_KP12_2_3] = <replace>);

benchmarks/models/Pipeline_KP12_2_5-EFwitness.imiprop

-(************************************************************
- *                      IMITATOR MODEL                      
- *
- * Producer/Consumer with n=2 processing nodes of length m=5
- *
- * Description     : The network presented in Figure 2 models the system consisting of the Producer feeding the Consumer with data sent through a sequence of nodes with additional processing capabilities. The model is scalable with respect to the number n of the processing nodes and the length m of each processing node and it contains three lower (a,c,e) and three upper (b,d,f) parameters. Note: the clocks were renamed (w.r.t. to [KP12]) for sake of simplicity.
- * Correctness     : φ2 = ConsWaiting ∧ ProdReady ∧ xtotal ≥ 5
- * Source          : SMT-based Parameter Synthesis for L/U Automata, Michał Knapik and Wojciech Penczek
- * Author          : Michał Knapik and Wojciech Penczek
- * Modeling        : Michał Knapik and Wojciech Penczek
- * Input by        : Étienne André
- *
- * Created         : 2020/08/18
- * Last modified   : 2020/08/18
- *
- * IMITATOR version: 3
- ************************************************************)
-
-(************************************************************)
-(* Property specification *)
-(************************************************************)
-
-(* φ2 = ConsWaiting ∧ ProdReady ∧ xtotal ≥ 5 *)
-property := #witness EF(loc[Consumer] = consWaiting & loc[Producer] = prodReady (*& xtotal >= 5*) & loc[observer] = finished);

benchmarks/models/Pipeline_KP12_3_2-EFwitness.imiprop

-(************************************************************
- *                      IMITATOR MODEL                      
- *
- * Producer/Consumer with n=3 processing nodes of length m=2
- *
- * Description     : The network presented in Figure 2 models the system consisting of the Producer feeding the Consumer with data sent through a sequence of nodes with additional processing capabilities. The model is scalable with respect to the number n of the processing nodes and the length m of each processing node and it contains three lower (a,c,e) and three upper (b,d,f) parameters. Note: the clocks were renamed (w.r.t. to [KP12]) for sake of simplicity.
-	WARNING: most of the valuations in [KP12] do not match the result of IMITATOR!
- * Correctness     : φ2 = ConsWaiting ∧ ProdReady ∧ xtotal ≥ 5
- * Source          : SMT-based Parameter Synthesis for L/U Automata, Michał Knapik and Wojciech Penczek
- * Author          : Michał Knapik and Wojciech Penczek
- * Modeling        : Michał Knapik and Wojciech Penczek
- * Input by        : Étienne André
- *
- * Created         : 2020/08/18
- * Last modified   : 2020/08/18
- *
- * IMITATOR version: 3
- ************************************************************)
-
-(************************************************************)
-(* Property specification *)
-(************************************************************)
-
-(* φ2 = ConsWaiting ∧ ProdReady ∧ xtotal ≥ 5 *)
-property := #witness EF(loc[Consumer] = consWaiting & loc[Producer] = prodReady (*& xtotal >= 5*) & loc[observer] = finished);

benchmarks/models/Pipeline_KP12_3_3-EFwitness.imiprop

-(************************************************************
- *                      IMITATOR MODEL                      
- *
- * Producer/Consumer with n=3 processing nodes of length m=3
- *
- * Description     : The network presented in Figure 2 models the system consisting of the Producer feeding the Consumer with data sent through a sequence of nodes with additional processing capabilities. The model is scalable with respect to the number n of the processing nodes and the length m of each processing node and it contains three lower (a,c,e) and three upper (b,d,f) parameters. Note: the clocks were renamed (w.r.t. to [KP12]) for sake of simplicity.
-	WARNING: the first of the valuations in [KP12] does not match the result of IMITATOR!
- * Correctness     : φ2 = ConsWaiting ∧ ProdReady ∧ xtotal ≥ 5
- * Source          : SMT-based Parameter Synthesis for L/U Automata, Michał Knapik and Wojciech Penczek
- * Author          : Michał Knapik and Wojciech Penczek
- * Modeling        : Michał Knapik and Wojciech Penczek
- * Input by        : Étienne André
- *
- * Created         : 2020/08/18
- * Last modified   : 2020/08/18
- *
- * IMITATOR version: 3
- ************************************************************)
-
-(************************************************************)
-(* Property specification *)
-(************************************************************)
-
-(* φ2 = ConsWaiting ∧ ProdReady ∧ xtotal ≥ 5 *)
-property := #witness EF(loc[Consumer] = consWaiting & loc[Producer] = prodReady (*& xtotal >= 5*) & loc[observer] = finished);

benchmarks/models/RCP-EFwitness.imiprop

-property := #witness EF(loc[RCP] = <replace>);

benchmarks/models/accel-1000-EFwitness.imiprop

-(************************************************************
- *                      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 *)
-(************************************************************)
-
-(* Network of PTA *)
-(* property := #witness EF(loc[pta] = s_end); *)
-
-(* Sync Product *)
-property := #witness EF(loc[accel_1000] = <replace>);

benchmarks/models/accel-10000-EFwitness.imiprop

-(************************************************************
- *                      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 := #witness EF(loc[pta] = s_end);
-(* property := #witness EF(loc[accel_10000] = <replace>); *)

benchmarks/models/accel-2000-EFwitness.imiprop

-(************************************************************
- *                      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 := #witness EF(loc[pta] = s_end);

benchmarks/models/accel-3000-EFwitness.imiprop

-(************************************************************
- *                      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 := #witness EF(loc[pta] = s_end);

benchmarks/models/accel-4000-EFwitness.imiprop

-(************************************************************
- *                      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 := #witness EF(loc[pta] = s_end);

benchmarks/models/accel-5000-EFwitness.imiprop

-(************************************************************
- *                      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 := #witness EF(loc[pta] = s_end);

benchmarks/models/accel-6000-EFwitness.imiprop

-(************************************************************
- *                      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 := #witness EF(loc[pta] = s_end);

benchmarks/models/accel-7000-EFwitness.imiprop

-(************************************************************
- *                      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 := #witness EF(loc[pta] = s_end);

benchmarks/models/accel-8000-EFwitness.imiprop

-(************************************************************
- *                      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 := #witness EF(loc[pta] = s_end);

benchmarks/models/accel-9000-EFwitness.imiprop

-(************************************************************
- *                      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 := #witness EF(loc[pta] = s_end);

benchmarks/models/blowup-1000-EFwitness.imiprop

-(************************************************************
- *                      IMITATOR MODEL                      
- *
- * Parametric timed pattern matching benchmark: blowup (designed on purpose to test the limits of our algorithm)
- *
- * Description     : Template of a timed word alternating between a and c
- * Correctness     : N/A
- * Source          : Étienne André, Ichiro Husuo, Masaki Waga "Offline timed pattern matching under uncertainty" (ICECCS 2018)
- * Author          : Étienne André and Masaki Waga
- * Modeling        : Étienne André and Masaki Waga
- * 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 := #witness EF(loc[pta] = s3);

benchmarks/models/blowup-200-EFwitness.imiprop

-(************************************************************
- *                      IMITATOR MODEL
- *
- * Parametric timed pattern matching benchmark: blowup (designed on purpose to test the limits of our algorithm)
- *
- * Description     : Template of a timed word alternating between a and c
- * Correctness     : N/A
- * Source          : Étienne André, Ichiro Husuo, Masaki Waga "Offline timed pattern matching under uncertainty" (ICECCS 2018)
- * Author          : Étienne André and Masaki Waga
- * Modeling        : Étienne André and Masaki Waga
- * 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 := #witness EF(loc[pta] = s3); *)
-property := #witness EF(loc[blowup_200] = <replace>);

benchmarks/models/blowup-400-EFwitness.imiprop

-(************************************************************
- *                      IMITATOR MODEL
- *
- * Parametric timed pattern matching benchmark: blowup (designed on purpose to test the limits of our algorithm)
- *
- * Description     : Template of a timed word alternating between a and c
- * Correctness     : N/A
- * Source          : Étienne André, Ichiro Husuo, Masaki Waga "Offline timed pattern matching under uncertainty" (ICECCS 2018)
- * Author          : Étienne André and Masaki Waga
- * Modeling        : Étienne André and Masaki Waga
- * 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 := #witness EF(loc[pta] = s3); *)
-property := #witness EF(loc[blowup_400] = <replace>);