From 57fa1c8b5f95ed959e5d39794950f0140c4a78a6 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 24 May 2004 11:53:57 +0000
Subject: [PATCH] * iface/gspn/ssp.hh (gspn_ssp_interface::gspn_ssp_interface):
 Add the `inclusion' flag. * iface/gspn/ssp.cc
 (gspn_ssp_interface::gspn_ssp_interface): Call inclusion_version when
 inclusion is set. * iface/gspn/ltlgspn.cc (main) [SSP]: Turn on inclusion for
 -e3, -e4, and -e5.

---
 ChangeLog             |  9 +++++++++
 iface/gspn/ltlgspn.cc |  3 ++-
 iface/gspn/ssp.cc     | 10 +++++++---
 iface/gspn/ssp.hh     |  3 ++-
 4 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 1877ebb1a..b3d7c2c3a 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,12 @@
+2004-05-24  Soheib Baarir  <Souheib.Baarir@lip6.fr>
+
+	* iface/gspn/ssp.hh (gspn_ssp_interface::gspn_ssp_interface): Add
+	the `inclusion' flag.
+	* iface/gspn/ssp.cc (gspn_ssp_interface::gspn_ssp_interface): Call
+	inclusion_version when inclusion is set.
+	* iface/gspn/ltlgspn.cc (main) [SSP]: Turn on inclusion for -e3,
+	-e4, and -e5.
+
 2004-05-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* iface/gspn/gspn.cc (tgba_gspn_private_): Define alive_prop,
diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc
index e8bae46d5..01a5e55cd 100644
--- a/iface/gspn/ltlgspn.cc
+++ b/iface/gspn/ltlgspn.cc
@@ -174,7 +174,8 @@ main(int argc, char **argv)
       spot::bdd_dict* dict = new spot::bdd_dict();
 
 #if SSP
-      spot::gspn_ssp_interface gspn(2, argv, dict, env);
+      bool inclusion = (check != Couvreur && check != Couvreur2);
+      spot::gspn_ssp_interface gspn(2, argv, dict, env, inclusion);
 
       spot::tgba_parse_error_list pel1;
       spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2],
diff --git a/iface/gspn/ssp.cc b/iface/gspn/ssp.cc
index 9066ab73c..1943afa87 100644
--- a/iface/gspn/ssp.cc
+++ b/iface/gspn/ssp.cc
@@ -385,7 +385,7 @@ namespace spot
             state_array = (state**) realloc(state_array,
 					    (size_states + 1) * sizeof(state*));
 	    state_array[size_states] = i->current_state();
-	    props_[nb_arc_props].arc->curr_state  = size_states;
+	    props_[nb_arc_props].arc->curr_state = size_states;
             size_states++;
 
 	    while (all_conds_ != bddfalse)
@@ -533,10 +533,14 @@ namespace spot
   //////////////////////////////////////////////////////////////////////
 
   gspn_ssp_interface::gspn_ssp_interface(int argc, char **argv,
-					     bdd_dict* dict,
-					     const gspn_environment& env)
+					 bdd_dict* dict,
+					 const gspn_environment& env,
+					 bool inclusion)
     : dict_(dict), env_(env)
   {
+    if (inclusion)
+      inclusion_version();
+
     int res = initialize(argc, argv);
     if (res)
       throw gspn_exeption("initialize()", res);
diff --git a/iface/gspn/ssp.hh b/iface/gspn/ssp.hh
index d525d771a..8fab892f1 100644
--- a/iface/gspn/ssp.hh
+++ b/iface/gspn/ssp.hh
@@ -38,7 +38,8 @@ namespace spot
   {
   public:
     gspn_ssp_interface(int argc, char **argv,
-			 bdd_dict* dict, const gspn_environment& env);
+		       bdd_dict* dict, const gspn_environment& env,
+		       bool inclusion = false);
     ~gspn_ssp_interface();
     tgba* automaton(const tgba* operand) const;
   private: