* iface/gspn/gspn.cc (tgba_gspn_private_): Define alive_prop,

and dead_prop from the dead argument passed to the constructor.
(tgba_succ_iterator_gspn): Stutter on dead transitions.
(tgba_gspn::tgba_gspn): Hand dead to tgba_gspn_private_.
(gspn_interface::gspn_interface): Hand dead to tgba_gspn.
* iface/gspn/gspn.hh (gspn_interface::gspn_interface): Take a
dead argument.
* iface/gspn/ltlgspn.cc [!SSP]: Add a option -d to specify the
dead property.
* iface/gspn/udcseltl.test: Try option -d.

ChangeLog

@@ -1,5 +1,16 @@
 2004-05-21  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* iface/gspn/gspn.cc (tgba_gspn_private_): Define alive_prop,
+	and dead_prop from the dead argument passed to the constructor.
+	(tgba_succ_iterator_gspn): Stutter on dead transitions.
+	(tgba_gspn::tgba_gspn): Hand dead to tgba_gspn_private_.
+	(gspn_interface::gspn_interface): Hand dead to tgba_gspn.
+	* iface/gspn/gspn.hh (gspn_interface::gspn_interface): Take a
+	dead argument.
+	* iface/gspn/ltlgspn.cc [!SSP]: Add a option -d to specify the
+	dead property.
+	* iface/gspn/udcseltl.test: Try option -d.
+
 	* src/sanity/style.test: Check the iface/ tree too.
 	* iface/gspn/gspn.cc, iface/gspn/ssp.cc: Fix style.
 

iface/gspn/gspn.cc

@@ -89,9 +89,11 @@ namespace spot
     size_t index_count;
     const state_gspn* last_state_conds_input;
     bdd last_state_conds_output;
+    bdd alive_prop;
+    bdd dead_prop;
 
-
+    tgba_gspn_private_(bdd_dict* dict, gspn_environment& env,
-    tgba_gspn_private_(bdd_dict* dict, const gspn_environment& env)
+		       const std::string& dead)
       : refs(1), dict(dict), all_indexes(0), last_state_conds_input(0)
     {
       const gspn_environment::prop_map& p = env.get_prop_map();
@@ -101,6 +103,11 @@ namespace spot
 	  for (gspn_environment::prop_map::const_iterator i = p.begin();
 	       i != p.end(); ++i)
 	    {
+	      // Skip the DEAD proposition, GreatSPN knows nothing
+	      // about it.
+	      if (i->first == dead)
+		continue;
+
 	      int var = dict->register_proposition(i->second, this);
 	      AtomicProp index;
 	      int err = prop_index(i->first.c_str(), &index);
@@ -129,6 +136,38 @@ namespace spot
 	  dict->unregister_all_my_variables(this);
 	  throw;
 	}
+
+      // Register the "dead" proposition.  There are three cases to
+      // consider:
+      //  * If DEAD is "false", it means we are not interested in finite
+      //    sequences of the system.
+      //  * If DEAD is "true", we want to check finite sequences as well
+      //    as infinite sequences, but do not need to distinguish them.
+      //  * If DEAD is any other string, this is the name a property
+      //    that should be true when looping on a dead state, and false
+      //    otherwise.
+      // We handle these three case by setting ALIVE_PROP and DEAD_PROP
+      // appropriately.  ALIVE_PROP is the bdd that should be ANDed
+      // to all transitions leaving a live state, while DEAD_PROP should
+      // bdd ANDed to all transitions leaving a dead state.
+      if (!strcasecmp(dead.c_str(), "false"))
+	{
+	  alive_prop = bddtrue;
+	  dead_prop = bddfalse;
+	}
+      else if (!strcasecmp(dead.c_str(), "true"))
+	{
+	  alive_prop = bddtrue;
+	  dead_prop = bddtrue;
+	}
+      else
+	{
+	  ltl::formula* f = env.require(dead);
+	  assert(f);
+	  int var = dict->register_proposition(f, this);
+	  dead_prop = bdd_ithvar(var);
+	  alive_prop = bdd_nithvar(var);
+	}
     }
 
     tgba_gspn_private_::~tgba_gspn_private_()
@@ -193,20 +232,21 @@ namespace spot
 	successors_(0),
 	size_(0),
 	current_(0),
-	data_(data)
+	data_(data),
+	from_state_(state)
     {
       int res = succ(state, &successors_, &size_);
       if (res)
 	throw gspn_exeption("succ()", res);
-      assert(successors_);
+      // GreatSPN should return successors_ == 0 and size_ == 0 when a
-      // GSPN is expected to return a looping "dead" transition where
+      // state has no successors.
-      // there is no successor.
+      assert((size_ <= 0) ^ (successors_ != 0));
-      assert(size_ > 0);
     }
 
     virtual
     ~tgba_succ_iterator_gspn()
     {
+      if (successors_)
 	succ_free(successors_);
     }
 
@@ -232,14 +272,23 @@ namespace spot
     virtual state*
     current_state() const
     {
-      return new state_gspn(successors_[current_].s);
+      // If GreatSPN returned no successor, we stutter on the dead state.
+      return
+	new state_gspn(successors_ ? successors_[current_].s : from_state_);
     }
 
     virtual bdd
     current_condition() const
+    {
+      if (successors_)
 	{
 	  bdd p = data_->index_to_bdd(successors_[current_].p);
-      return state_conds_ & p;
+	  return state_conds_ & p & data_->alive_prop;
+	}
+      else
+	{
+	  return state_conds_ & data_->dead_prop;
+	}
     }
 
     virtual bdd
@@ -254,6 +303,7 @@ namespace spot
     size_t size_;		/// size of successors_
     size_t current_;		/// current position in successors_
     tgba_gspn_private_* data_;
+    State from_state_;
   }; // tgba_succ_iterator_gspn
 
 
@@ -269,7 +319,8 @@ namespace spot
   class tgba_gspn: public tgba
   {
   public:
-    tgba_gspn(bdd_dict* dict, const gspn_environment& env);
+    tgba_gspn(bdd_dict* dict, gspn_environment& env,
+	      const std::string& dead);
     tgba_gspn(const tgba_gspn& other);
     tgba_gspn& operator=(const tgba_gspn& other);
     virtual ~tgba_gspn();
@@ -290,9 +341,10 @@ namespace spot
   };
 
 
-  tgba_gspn::tgba_gspn(bdd_dict* dict, const gspn_environment& env)
+  tgba_gspn::tgba_gspn(bdd_dict* dict, gspn_environment& env,
+		       const std::string& dead)
   {
-    data_ = new tgba_gspn_private_(dict, env);
+    data_ = new tgba_gspn_private_(dict, env, dead);
   }
 
   tgba_gspn::tgba_gspn(const tgba_gspn& other)
@@ -410,8 +462,9 @@ namespace spot
   //////////////////////////////////////////////////////////////////////
 
   gspn_interface::gspn_interface(int argc, char **argv,
-				 bdd_dict* dict, const gspn_environment& env)
+				 bdd_dict* dict, gspn_environment& env,
-    : dict_(dict), env_(env)
+				 const std::string& dead)
+    : dict_(dict), env_(env), dead_(dead)
   {
     int res = initialize(argc, argv);
     if (res)
@@ -428,9 +481,7 @@ namespace spot
   tgba*
   gspn_interface::automaton() const
   {
-    return new tgba_gspn(dict_, env_);
+    return new tgba_gspn(dict_, env_, dead_);
   }
 
-
-
 }

iface/gspn/gspn.hh

@@ -36,12 +36,14 @@ namespace spot
   {
   public:
     gspn_interface(int argc, char **argv,
-		   bdd_dict* dict, const gspn_environment& env);
+		   bdd_dict* dict, gspn_environment& env,
+		   const std::string& dead = "true");
     ~gspn_interface();
     tgba* automaton() const;
   private:
     bdd_dict* dict_;
-    const gspn_environment& env_;
+    gspn_environment& env_;
+    const std::string dead_;
   };
 }
 

iface/gspn/ltlgspn.cc

@@ -52,6 +52,12 @@ syntax(char* prog)
 	    << "  -c  compute an example" << std::endl
 	    << "      (instead of just checking for emptiness)" << std::endl
 	    << std::endl
+#ifndef SSP
+            << "  -d DEAD" << std::endl
+            << "      use DEAD as property for marking dead states"
+	    << " (by default DEAD=true)" << std::endl
+#endif
+
 	    << "  -e  use Couvreur's emptiness-check (default)" << std::endl
 	    << "  -e2 use Couvreur's emptiness-check's shy variant" << std::endl
 #ifdef SSP
@@ -81,6 +87,7 @@ main(int argc, char **argv)
       enum { Lacim, Fm } trans = Lacim;
       bool compute_counter_example = false;
       bool proj = true;
+      std::string dead = "true";
 
       spot::gspn_environment env;
 
@@ -90,6 +97,17 @@ main(int argc, char **argv)
 	    {
 	      compute_counter_example = true;
 	    }
+#ifndef SSP
+	  else if (!strcmp(argv[formula_index], "-d"))
+	    {
+	      if (formula_index + 1 >= argc)
+		syntax(argv[0]);
+	      dead = argv[++formula_index];
+	      if (strcasecmp(dead.c_str(), "true")
+		  && strcasecmp(dead.c_str(), "false"))
+		env.declare(dead);
+	    }
+#endif
 	  else if (!strcmp(argv[formula_index], "-e"))
 	    {
 	      check = Couvreur;
@@ -164,7 +182,7 @@ main(int argc, char **argv)
       if (spot::format_tgba_parse_errors(std::cerr, pel1))
 	return 2;
 #else
-      spot::gspn_interface gspn(2, argv, dict, env);
+      spot::gspn_interface gspn(2, argv, dict, env, dead);
 #endif
 
       spot::tgba* a_f = 0;

iface/gspn/udcseltl.test

@@ -20,7 +20,8 @@ chmod +w udcs
 # !G(ReP1 => F(gsP1)) is false
 ../ltlgspn-srg -c -l -e udcs/udcs \
   '!G(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1
-../ltlgspn-srg -c -l -e2 udcs/udcs \
+../ltlgspn-srg -d dead -c -l -e2 udcs/udcs \
   '!G(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1
-
+grep 'dead:0' output
+grep 'dead:1' output && exit 1
 :