From 2580fc6f91d44471159056b4a72fd3ffa4aed03a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 10 Jan 2013 18:42:36 +0100
Subject: [PATCH] * src/tgbatest/babiak.test: Rewrite using ltlcross.

---
 src/tgbatest/babiak.test | 80 ++++------------------------------------
 1 file changed, 8 insertions(+), 72 deletions(-)

diff --git a/src/tgbatest/babiak.test b/src/tgbatest/babiak.test
index dfcdab0a4..32dbfe87f 100755
--- a/src/tgbatest/babiak.test
+++ b/src/tgbatest/babiak.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -27,7 +27,6 @@
 # buildfarm will timeout if it does).
 
 . ./defs
-need_lbtt
 
 set -e
 
@@ -40,73 +39,10 @@ X((X(!p1 V F!p6)V F!p4)U p2)&(F(G((0 U(F p6))U((p1 U(G(p4 U F p0)))U X p7))))
 (G(G(((F p5)U((((F!p1)V(p2 &!p4))|!p2)|((X!p7 U!p4)V(F(F((G p2)&p5))))))U p6)))
 EOF
 
-cat > config <<EOF
-Algorithm
-{
-   Name = "Spot/FM basic"
-   Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot '../ltl2tgba -F -f -t'"
-   Enabled = yes
-}
+ltl2tgba=../ltl2tgba
 
-Algorithm
-{
-   Name = "Spot/FM, with reductions + degeneralization (neverclaim)"
-   Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spin '../ltl2tgba -r4 -R3f -F -f -N'"
-   Enabled = yes
-}
-
-Algorithm
-{
-   Name = "Spot/FM, with reducetion + WDBA + degeneralization (neverclaim)"
-   Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spin '../ltl2tgba -r7 -R3 -f -x -N -F -Rm'"
-   Enabled = yes
-}
-
-Algorithm
-{
-   Name = "Spot/FM, with reducetion + WDBA + degeneralization (DS)"
-   Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot '../ltl2tgba -r7 -R3 -f -x -DS -t -F -Rm'"
-   Enabled = yes
-}
-
-GlobalOptions
-{
-   Rounds = 6
-   Interactive = Never
-#   Verbosity = 5
-#   ComparisonCheck = no
-#   ConsistencyCheck = no
-#   IntersectionCheck = no
-}
-
-# Not used, but LBTT seems to want it.
-FormulaOptions
-{
-  Size = 1...13
-  Propositions = 6
-
-  AbbreviatedOperators = Yes
-  GenerateMode = Normal
-  OutputMode = Normal
-  PropositionPriority = 50
-
-  TruePriority = 1
-  FalsePriority = 1
-
-  AndPriority = 10
-  OrPriority = 10
-  XorPriority = 0
-  # EquivalencePriority = 0
-
-  BeforePriority = 0
-
-  DefaultOperatorPriority = 5
-}
-EOF
-
-${LBTT} --formulafile=formulae
-rm config
+../../bin/ltlcross <formulae \
+  "$ltl2tgba -t %f >%T" \
+  "$ltl2tgba -N -r4 -R3f %f >%N" \
+  "$ltl2tgba -N -r7 -R3 -x -Rm %f >%N" \
+  "$ltl2tgba -t -r7 -R3 -f -x -DS -Rm %f >%T"