espresso stuff

src/main.cc

@@ -134,11 +134,12 @@ int main(int argc, char** argv)
     }
     if (!exec_opt.ofilepath.empty())
     {
-      oput_protocon_file (exec_opt.ofilepath,
-                          sys, *o_topology,
-                          sys.actions,
-                          exec_opt.use_espresso,
-                          exec_opt.argline.c_str());
+      oput_protocon_file
+        (exec_opt.ofilepath,
+         sys, *o_topology,
+         sys.actions,
+         exec_opt.maybe_espresso,
+         exec_opt.argline.c_str());
     }
   }
   std::cerr.flush();

src/opt.cc

@@ -540,7 +540,10 @@ protocon_options_rec
       exec_opt.ofilepath = pathname2(relpath, argv[argi++]);
     }
     else if (eq_cstr (arg, "-espresso")) {
-      exec_opt.use_espresso = true;
+      if (!argv[argi]) {
+        failout_sysCx("Not enuff arguments.");
+      }
+      exec_opt.maybe_espresso = argv[argi++];
     }
     else if (eq_cstr (arg, "-x-test-known")) {
       Xn::Sys test_sys;

src/opt.hh

@@ -58,7 +58,7 @@ public:
   std::string log_ofilename;
   std::string xfilepath;
   std::string ofilepath;
-  bool use_espresso;
+  std::string maybe_espresso;
   std::vector<std::string> xfilepaths;
   std::string model_ofilepath;
   std::string graphviz_ofilepath;
@@ -75,7 +75,6 @@ public:
   ProtoconOpt()
     : task(SearchTask)
     , nparallel( 1 )
-    , use_espresso( false )
     , only_udp_include( false )
     , conflict_order( HiLoOrder )
   {}

src/pla.cc

@@ -260,11 +260,12 @@ oput_protocon_pc_acts_espresso_spawn(std::ostream& out, const Xn::PcSymm& pc_sym
   bool
 oput_protocon_pc_acts_espresso(std::ostream& out,
                                const Xn::PcSymm& pc_symm,
-                               const std::vector<Xn::ActSymm>& acts)
+                               const std::vector<Xn::ActSymm>& acts,
+                               const std::string& espresso_name)
 {
   const char* const argv[] = {
 #if 1
-    "espresso",
+    espresso_name.c_str(),
     // Using -Dexact can take a long time.
     // "-Dexact",
 #else

src/pla.hh

@@ -2,6 +2,7 @@
 #ifndef PLA_HH_
 #define PLA_HH_
 #include <ostream>
+#include <string>
 #include <vector>
 
 #include "namespace.hh"
@@ -14,9 +15,11 @@ oput_pla_file(std::ostream& ofile, const Xn::Sys& sys);
 bool
 oput_pla_file(const std::string& ofilename, const Xn::Sys& sys);
 bool
-oput_protocon_pc_acts_espresso(std::ostream& ofile,
-                               const Xn::PcSymm& pc_symm,
-                               const std::vector<Xn::ActSymm>& acts);
+oput_protocon_pc_acts_espresso(
+    std::ostream& out,
+    const Xn::PcSymm& pc_symm,
+    const std::vector<Xn::ActSymm>& acts,
+    const std::string& espresso_name);
 
 END_NAMESPACE
 #endif

src/prot-ofile.cc

@@ -146,7 +146,7 @@ static
   bool
 oput_protocon_pc_acts(std::ostream& out, const Xn::PcSymm& pc_symm,
                       const std::vector<Xn::ActSymm>& acts,
-                      bool use_espresso)
+                      const std::string& maybe_espresso)
 {
   const Xn::PcSymmSpec& pc_symm_spec = *pc_symm.spec;
   if (pc_symm_spec.shadow_act_strings.sz() > 0) {
@@ -196,8 +196,8 @@ oput_protocon_pc_acts(std::ostream& out, const Xn::PcSymm& pc_symm,
   out << "\n  puppet:";
 
   bool good = true;
-  if (use_espresso) {
-    good = oput_protocon_pc_acts_espresso(out, pc_symm, acts);
+  if (!maybe_espresso.empty()) {
+    good = oput_protocon_pc_acts_espresso(out, pc_symm, acts, maybe_espresso);
   }
   else {
     for (const auto& act : acts) {
@@ -302,7 +302,7 @@ oput_protocon_pc_invariant(std::ostream& out, const Xn::PcSymm& pc_symm,
 oput_protocon_file(std::ostream& out, const Xn::Sys& sys,
                    const Xn::Net& o_topology,
                    const vector<uint>& actions,
-                   bool use_espresso,
+                   const std::string& maybe_espresso,
                    const char* comment)
 {
   DeclLegit( good );
@@ -380,7 +380,7 @@ oput_protocon_file(std::ostream& out, const Xn::Sys& sys,
     DoLegitLine("output invariant")
       oput_protocon_pc_invariant(out, pc_symm, style_str);
     DoLegitLine("output actions")
-      oput_protocon_pc_acts(out, pc_symm, acts, use_espresso);
+      oput_protocon_pc_acts(out, pc_symm, acts, maybe_espresso);
     out << "\n}\n";
   }
 
@@ -389,16 +389,16 @@ oput_protocon_file(std::ostream& out, const Xn::Sys& sys,
 
   bool
 oput_protocon_file(std::ostream& out, const Xn::Sys& sys, const vector<uint>& actions,
-                   bool use_espresso, const char* comment)
+                   const std::string& maybe_espresso, const char* comment)
 {
-  return oput_protocon_file(out, sys, sys.topology, actions, use_espresso, comment);
+  return oput_protocon_file(out, sys, sys.topology, actions, maybe_espresso, comment);
 }
 
   bool
 oput_protocon_file(std::ostream& out, const Xn::Sys& sys,
-                   bool use_espresso, const char* comment)
+                   const std::string& maybe_espresso, const char* comment)
 {
-  return oput_protocon_file(out, sys, sys.actions, use_espresso, comment);
+  return oput_protocon_file(out, sys, sys.actions, maybe_espresso, comment);
 }
 
   bool
@@ -407,22 +407,23 @@ oput_protocon_file(
     const Xn::Sys& sys,
     const Xn::Net& o_topology,
     const vector<uint>& actions,
-    bool use_espresso,
+    const std::string& maybe_espresso,
     const char* comment)
 {
   fildesh::ofstream out(ofilename.c_str());
   if (!out.good()) {return false;}
-  return oput_protocon_file(out, sys, o_topology, actions, use_espresso, comment);
+  return oput_protocon_file(out, sys, o_topology, actions, maybe_espresso, comment);
 }
 
   bool
 oput_protocon_file(
     const std::string& ofilename,
     const Xn::Sys& sys,
-    bool use_espresso,
+    const std::string& maybe_espresso,
     const char* comment)
 {
-  return oput_protocon_file (ofilename, sys, sys.topology, sys.actions, use_espresso, comment);
+  return oput_protocon_file(
+      ofilename, sys, sys.topology, sys.actions, maybe_espresso, comment);
 }
 
 END_NAMESPACE

src/prot-ofile.hh

@@ -7,23 +7,35 @@
 #include "namespace.hh"
 
 bool
-oput_protocon_file(std::ostream& out, const Xn::Sys& sys,
-                   const Xn::Net& o_topology,
-                   const vector<uint>& actions,
-                   bool use_espresso, const char* comment);
+oput_protocon_file(
+    std::ostream& out,
+    const Xn::Sys& sys, const Xn::Net& o_topology, const vector<uint>& actions,
+    const std::string& maybe_espresso,
+    const char* comment);
 bool
-oput_protocon_file(std::ostream& out, const Xn::Sys& sys, const vector<uint>& actions,
-                   bool use_espresso, const char* comment);
+oput_protocon_file(
+    std::ostream& out,
+    const Xn::Sys& sys, const vector<uint>& actions,
+    const std::string& maybe_espresso,
+    const char* comment);
 bool
-oput_protocon_file(std::ostream& out, const Xn::Sys& sys,
-                   bool use_espresso, const char* comment);
+oput_protocon_file(
+    std::ostream& out,
+    const Xn::Sys& sys,
+    const std::string& maybe_espresso,
+    const char* comment);
 bool
-oput_protocon_file(const std::string& ofilename,
-                   const Xn::Sys& sys, const Xn::Net& o_topology,  const vector<uint>& actions,
-                   bool use_espresso, const char* comment);
+oput_protocon_file(
+    const std::string& ofilename,
+    const Xn::Sys& sys, const Xn::Net& o_topology,  const vector<uint>& actions,
+    const std::string& maybe_espresso,
+    const char* comment);
 bool
-oput_protocon_file(const std::string& ofilename, const Xn::Sys& sys,
-                   bool use_espresso, const char* comment);
+oput_protocon_file(
+    const std::string& ofilename,
+    const Xn::Sys& sys,
+    const std::string& maybe_espresso,
+    const char* comment);
 
 END_NAMESPACE
 #endif

src/search.cc

@@ -47,7 +47,7 @@ verify_solutions(const PartialSynthesis& inst, StabilizationCkInfo* info, uint*
 
         fildesh::ofstream livelock_out(livelock_out_filename.c_str());
         oput_protocon_file(livelock_out, *inst.ctx->systems[i], inst[i].actions,
-                           false, "livelock");
+                           "", "livelock");
       }
       *inst[i].log << "Solution was NOT self-stabilizing." << std::endl;
       return false;
@@ -686,7 +686,7 @@ void
         log << "Writing system to: " << filepath  << std::endl;
         fildesh::ofstream prot_out(filepath.c_str());
         oput_protocon_file(prot_out, sys, sys.actions,
-                           exec_opt.use_espresso,
+                           exec_opt.maybe_espresso,
                            exec_opt.argline.c_str());
       }
     }
@@ -949,7 +949,7 @@ stabilization_search(vector<uint>& ret_actions,
                std::to_string(PcIdx) + "." +
                std::to_string(trial_idx)).c_str());
           oput_protocon_file(prot_out, sys, actions,
-                             exec_opt.use_espresso,
+                             exec_opt.maybe_espresso,
                              exec_opt.argline.c_str());
         }
       }

src/synthesis.cc

@@ -1285,7 +1285,7 @@ PartialSynthesis::revise_actions_alone(Set<uint>& adds, Set<uint>& dels,
             this->ctx->opt.n_livelock_ofiles).c_str();
         this->ctx->opt.n_livelock_ofiles += 1;
         fildesh::ofstream livelock_out(livelock_out_filename.c_str());
-        oput_protocon_file(livelock_out, sys, this->actions, false, "livelock");
+        oput_protocon_file(livelock_out, sys, this->actions, "", "livelock");
       }
     }
     return false;

test/examplesoln/PLA_MatchRingThreeState_test.fildesh

@@ -4,7 +4,6 @@
 (: MatchRingThreeState_file Filename .self.opt.input_file)
 
 |< protocon -nop -x $(XOF MatchRingThreeState_file) -o-pla -
-|- tee /tmp/out2
 |- cmp $(XOF expect_file)
 |> stderr