From 633906e347ef74afcf6870d81b106bcd05214d75 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 21 Sep 2016 13:51:49 +0200 Subject: [PATCH] * bench/dtgbasat/README: Update references. --- bench/dtgbasat/README | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/bench/dtgbasat/README b/bench/dtgbasat/README index abf734b57..2bcdde37a 100644 --- a/bench/dtgbasat/README +++ b/bench/dtgbasat/README @@ -1,5 +1,14 @@ -These benchmarks are part of a submitted paper. Please -do contact us if you would like a draft of this paper. +This benchmark was used in the FORTE'14 paper "Mechanizing the +Minimization of Deterministic Generalized Büchi Automata", by +Souheib Baarir and Alexandre Duret-Lutz. The generated data +used in the paper are at + + https://www.lrde.epita.fr/~adl/forte14/ + +Note that the encoding used in the SAT-based minimization have evolved +since the paper, so if you want to reproduce exactly the benchmark +from the paper, you should download a copy of Spot 1.2.3. + To reproduce, follow these instructions: @@ -28,7 +37,7 @@ To reproduce, follow these instructions: This will read the formulas from file "formulas" and output a file "info.ltl", in which each formula is associated to a class (the ①, - ②, ②, and ④ of the paper), and a number of acceptance conditions + ②, ③, and ④ of the paper), and a number of acceptance conditions (the "m" of the paper). 7) Build a makefile to run all experiments