From 3faf00544580f6a2890b4aafc228b294546b885a Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Mon, 22 Oct 2018 20:28:23 +0100 Subject: [PATCH] Script for TGC --- in/scripts/gen_tgc_sc.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/in/scripts/gen_tgc_sc.py b/in/scripts/gen_tgc_sc.py index d132103..7736d8c 100755 --- a/in/scripts/gen_tgc_sc.py +++ b/in/scripts/gen_tgc_sc.py @@ -93,4 +93,11 @@ formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf) out += PROPERTY_STR.format("f2",formula) +# f3 +formula = "EF( proc0.approach" +for i in range(1, n): + formula += " AND proc{:d}.approach".format(i) +formula += " )" +out += PROPERTY_STR.format("f3",formula) + print(out)