add -W option to compiler to add read dependency for may write variables.

tools/compile.h

@@ -19,6 +19,7 @@ struct Compile {
     commandline::BoolOption *o_ltsmin;
     commandline::BoolOption *o_ltsmin_ltl;
     commandline::BoolOption *o_textbook;
+    commandline::BoolOption *o_may_write_add_read;
     commandline::Engine *cmd_compile;
     commandline::StandardParserWithMandatoryCommand &opts;
 
@@ -59,13 +60,13 @@ struct Compile {
     }
 
     void compileDve( std::string in, bool ltsmin, bool ltsmin_ltl,
-    											  bool textbook,
-    											  bool verbose ) {
+                      bool textbook, bool verbose, bool may_write_add_read ) {
     	if (textbook)
     		die( "Textbook LTL semantics not yet implemented." );
     	if (ltsmin && ltsmin_ltl)
             die( "Use -l OR -L." );
         dve_compiler compiler(ltsmin || ltsmin_ltl, ltsmin_ltl);
+        compiler.setMayReadAddWrite(may_write_add_read);
         compiler.read( in.c_str() );
         compiler.analyse();
 
@@ -93,7 +94,7 @@ struct Compile {
             die( "FATAL: cannot open input file " + input + " for reading" );
         if ( str::endsWith( input, ".dve" ) ) {
             compileDve( input, o_ltsmin->boolValue(), o_ltsmin_ltl->boolValue(),
-                               o_textbook->boolValue(), verbose );
+                               o_textbook->boolValue(), verbose, o_may_write_add_read->boolValue());
 #ifdef HAVE_MURPHI
         } else if ( str::endsWith( input, ".m" ) ) {
             compileMurphi( input );
@@ -118,6 +119,9 @@ struct Compile {
         o_textbook = cmd_compile->add< commandline::BoolOption >(
             "textbook", 't', "textbook", "",
             "ltsmin interface with textbook LTL semantics" );
+        o_may_write_add_read = cmd_compile->add< commandline::BoolOption >(
+            "may_write_add_read", 'W', "may_write_add_read", "",
+            "may write dependency also add a read dependency");
 
     }
 

tools/dvecompile.cpp

@@ -473,6 +473,9 @@ void dve_compiler::analyse_expression( dve_expression_t & expr, ext_transition_t
             } else {
                 // some expression, mark all & continue analysis
                 mark_dependency(expr.get_ident_gid(), state_creator_t::VARIABLE, -1, dep);
+				if (dep == ext_transition.sv_write && may_write_add_read) {
+                    mark_dependency(expr.get_ident_gid(), state_creator_t::VARIABLE, -1, ext_transition.sv_read);
+                }
                 if ((*expr.left()).get_operator() == T_ASSIGNMENT) {
                     analyse_expression(*expr.left(), ext_transition, ext_transition.sv_write);                    
                 } else if (dep == ext_transition.sv_write) {

tools/dvecompile.h

@@ -60,6 +60,7 @@ struct dve_compiler: public dve_explicit_system_t
     bool ltsmin_ltl; // divine LTL semantics in LTsmin successor generator
     bool many;
     int current_label;
+    bool may_write_add_read;
 
     bool have_property;
     map<size_int_t,map<size_int_t,vector<ext_transition_t> > > transition_map;
@@ -97,8 +98,9 @@ struct dve_compiler: public dve_explicit_system_t
         outline();
     }
 
-    dve_compiler(bool ltsmin, bool ltsmin_ltl, error_vector_t & evect=gerr)
-        : explicit_system_t(evect), dve_explicit_system_t(evect), current_label(0), m_indent( 0 ), ltsmin(ltsmin), ltsmin_ltl(ltsmin_ltl)
+    dve_compiler(bool ltsmin, bool ltsmin_ltl, error_vector_t & evect=gerr, bool may_write_add_read=false)
+        : explicit_system_t(evect), dve_explicit_system_t(evect), current_label(0), m_indent( 0 ), 
+            ltsmin(ltsmin), ltsmin_ltl(ltsmin_ltl), may_write_add_read(may_write_add_read)
     {}
     virtual ~dve_compiler() {}
 
@@ -217,6 +219,10 @@ struct dve_compiler: public dve_explicit_system_t
     void setVerbose( bool v ) {
         m_verbose = v;
     }
+    
+    void setMayReadAddWrite(bool w) {
+        may_write_add_read = w;        
+    }
 
     void yield_state();
     void new_output_state();