Add dump-json mode of state spaces.

src/element/element.h

@@ -69,4 +69,8 @@
 #include "variant.hpp"
 #include "vector.h"
 
+#include "json/conv.hpp"
+#include "json/exception.hpp"
+#include "json/value.hpp"
+
 #endif /* LMN_ELEMENT_H */

src/element/json/value.cpp

@@ -56,7 +56,7 @@ namespace json {
 // for variant
 namespace c17 = slim::element;
 
-namespace c14 = slim::element;  // for make_unique
+namespace c14 = slim::element; // for make_unique
 
 using namespace slim::element;
 
@@ -277,9 +277,10 @@ std::istream &operator>>(std::istream &in, value_type &value) {
 }
 
 struct pretty_printer {
+  unsigned int indent;
   std::ostream &os;
 
-  pretty_printer(std::ostream &os) : os(os) {}
+  pretty_printer(std::ostream &os) : os(os), indent(0) {}
 
   void operator()(const json::null &value) { os << "null"; }
   void operator()(const json::integer &value) { os << value.value; }
@@ -292,23 +293,48 @@ struct pretty_printer {
   }
   void operator()(const value_ptr<json::array> &value) {
     os << "[";
+
+    indent++;
     for (size_t i = 0; i < value->value.size(); i++) {
       if (i > 0)
-        os << ", ";
+        os << ",";
+      os << "\n";
+      print_indent();
       c17::visit(*this, value->value[i]);
     }
+    indent--;
+
+    if (!value->value.empty()) {
+      os << "\n";
+      print_indent();
+    }
     os << "]";
   }
   void operator()(const value_ptr<json::object> &value) {
     os << "{";
+
+    indent++;
     for (auto it = value->value.begin(); it != value->value.end(); ++it) {
       if (it != value->value.begin())
-        os << ", ";
+        os << ",";
+      os << "\n";
+      print_indent();
       os << "\"" << it->first << "\": ";
       c17::visit(*this, it->second);
     }
+    indent--;
+
+    if (!value->value.empty()) {
+      os << "\n";
+      print_indent();
+    }
     os << "}";
   }
+
+  void print_indent() {
+    for (int i = 0; i < indent; i++)
+      os << "  ";
+  }
 };
 
 std::ostream &operator<<(std::ostream &out, const json::value_type &value) {

src/element/json/value.hpp

@@ -98,8 +98,11 @@ template <class T> struct value_ptr {
   T *ptr_;
 };
 
-using value_type = c17::variant<null, integer, real, string, boolean,
-                                value_ptr<array>, value_ptr<object>>;
+using array_t = value_ptr<array>;
+using object_t = value_ptr<object>;
+
+using value_type =
+    c17::variant<null, integer, real, string, boolean, array_t, object_t>;
 
 struct null {
   operator std::nullptr_t() { return nullptr; }
@@ -148,6 +151,8 @@ struct object {
   object(std::unordered_map<std::string, value_type> &&v)
       : value(std::move(v)) {}
   operator std::unordered_map<std::string, value_type>() { return value; }
+
+  value_type &operator[](const std::string &key) { return value[key]; }
 };
 
 // throws json::syntax_error, json::overflow_error

src/env.cpp

@@ -140,7 +140,7 @@ LmnEnv::LmnEnv() {
   this->show_chr = FALSE;
   this->show_ruleset = TRUE;
   this->output_format = DEFAULT;
-  this->mc_dump_format = CUI;
+  this->mc_dump_format = MCdumpFormat::CUI;
   this->sp_dump_format = SP_NONE;
   this->nd = FALSE;
   this->ltl = FALSE;

src/lmntal.h

@@ -220,7 +220,7 @@ LMN_EXTERN void lmn_free(void *p);
 
 /* 階層グラフ構造の出力形式 */
 enum OutputFormat { DEFAULT = 1, DEV, DOT, JSON };
-enum MCdumpFormat { CUI, LaViT, Dir_DOT, LMN_FSM_GRAPH, LMN_FSM_GRAPH_MEM_NODE, LMN_FSM_GRAPH_HL_NODE };
+enum class MCdumpFormat { CUI, LaViT, Dir_DOT, LMN_FSM_GRAPH, LMN_FSM_GRAPH_MEM_NODE, LMN_FSM_GRAPH_HL_NODE, JSON };
 enum SPdumpFormat { SP_NONE, INCREMENTAL, LMN_SYNTAX };
 
 /* 最適化実行 */
@@ -551,6 +551,12 @@ static constexpr bool profile = true;
 #else
 static constexpr bool profile = false;
 #endif
+
+#ifdef KWBT_OPT
+static constexpr bool kwbt_opt = true;
+#else
+static constexpr bool kwbt_opt = false;
+#endif
 } // namespace config
 } // namespace slim
 

src/main.cpp

@@ -301,13 +301,13 @@ static void parse_options(int *optid, int argc, char *argv[]) {
       break;
     case 1100:
       lmn_env.output_format = DOT;
-      lmn_env.mc_dump_format = Dir_DOT;
+      lmn_env.mc_dump_format = MCdumpFormat::Dir_DOT;
       break;
     case 1101:
-      lmn_env.mc_dump_format = LMN_FSM_GRAPH_MEM_NODE;
+      lmn_env.mc_dump_format = MCdumpFormat::LMN_FSM_GRAPH_MEM_NODE;
       break;
     case 1102:
-      lmn_env.mc_dump_format = LaViT;
+      lmn_env.mc_dump_format = MCdumpFormat::LaViT;
       break;
     case 1103:
       lmn_env.sp_dump_format = INCREMENTAL;
@@ -317,12 +317,13 @@ static void parse_options(int *optid, int argc, char *argv[]) {
       break;
     case 1105:
       lmn_env.output_format = JSON;
+      lmn_env.mc_dump_format = MCdumpFormat::JSON;
       break;
     case 1106:
-      lmn_env.mc_dump_format = LMN_FSM_GRAPH;
+      lmn_env.mc_dump_format = MCdumpFormat::LMN_FSM_GRAPH;
       break;
     case 1107:
-      lmn_env.mc_dump_format = LMN_FSM_GRAPH_HL_NODE;
+      lmn_env.mc_dump_format = MCdumpFormat::LMN_FSM_GRAPH_HL_NODE;
       break;
     case 1200: /* jni interactive mode */
 #ifdef HAVE_JNI_H

src/verifier/Makefile.am

@@ -42,8 +42,7 @@ liblmn_verifier_a_SOURCES =                              \
 	visitlog.h                 \
 	stack_macro.h              \
 	state_dumper.cpp           \
-	mem_encode/decoder.cpp     mem_encode/binstr.cpp \
-	json.cpp
+	mem_encode/decoder.cpp     mem_encode/binstr.cpp
 
 
 EXTRA_DIST = $(PARSER_SOURCE) $(PARSER_HEADER)