用C++生成solidity语言描述的buchi自动机的初级经验

用C++生成solidity语言描述的buchi自动机的初级经验

我的项目rvtool()中增加了生成solidity语言格式的监控器的模块。

solidity特殊之处在于，它是运行在以太坊虚拟机环境中的。EVM和环境是隔离的，因此无法直接读取文件。所以rvtool中通过读取LTL文本生成监控器的方式无法直接照搬到solidity上面。rvtool中建立了表达自动机监控器的数据结构，对该数据结构的赋值是通过几个循环结构完成的。而这个部分无法在solidity代码中表达。将LTL转化为buchi自动机的算法库难以移植到solidity中，也得不偿失。所以，最好的实现办法就是直接生成已经写好的监控器，包括数据结构以及对它的初始化。
最后生成的solidity代码是这样的：

pragma solidity >=0.4.22 <0.6.0;contract monitor_automata {struct Word_set {string word;mapping(string => uint256) wordset;}struct Monitor_label {string label;string[] strlist;Word_set[] word_sets;int256 next_state;}struct Monitor_state {int256 own_state;int256 label_numbers;Monitor_label[] monitor_labels;}struct Monitor {int256 state_number;mapping(uint256 => Monitor_state) nodes;}Monitor monitor;Monitor_state monitor_state_0;Monitor_label monitor_label_0;Word_set ws_0;Monitor_label monitor_label_1;Word_set ws_1;Monitor_state monitor_state_1;Monitor_label monitor_label_2;Word_set ws_2;function Monitor_init() public {//对数据结构的初始化，无法用循环结构表达//=================monitor_state_0.own_state = 0;monitor_label_0.label = "!event3";monitor__state = 0;ws_0.word = "!event3";ws_0.wordset["event3"] = 0;monitor_label_0.word_sets.push(ws_0);monitor_itor_labels.push(monitor_label_0);monitor_label_1.label = "event3";monitor__state = 1;ws_1.word = "event3";ws_1.wordset["event3"] = 1;monitor_label_1.word_sets.push(ws_1);monitor_itor_labels.push(monitor_label_1);monitor_state_0.label_numbers = des[0] = monitor_state_0;//=================monitor_state_1.own_state = 1;monitor_label_2.label = "!event1 & !event3 & event4";monitor__state = 0;ws_2.word = "!event1 & !event3 & event4";ws_2.wordset["event1"] = 0;ws_2.wordset["event3"] = 0;ws_2.wordset["event4"] = 1;monitor_label_2.word_sets.push(ws_2);monitor_itor_labels.push(monitor_label_2);monitor_state_1.label_numbers = des[1] = monitor_state_1;}//将输入的字符串解析为数据结构。然后将其
}

代码生成分为3步： 1、生成固定结构的结构体2、生成结构体变量的声明语句3、生成对结构体变量进行赋值的语句。

function Monitor_init()实现的是对该数据结构的初始化，它无法用循环结构来表达，因为这里并没有编写solidity解析LTL公式的模块。
采用直接生成"声明并逐一对数据结构变量进行初始化"代码的办法。针对rvtool中的循环结构中的同名变量，我使用了后缀编号的方式。
例如

//int m = 0;for (auto &t : label_set){Word_set ws;string ws_m = "ws_"+m;ofile<<"        Word_set  ws_"<<m<<";n";m++;}

这个循环结构中，程序声明了Word_set ws这个结构体变量，然而它是在内存中完成的，是linux环境，它是无法在solidity的EVM环境中使用的。
于是在这个循环体中加入了 ofile<<" Word_set ws_"<< m<<";n";语句，该语句将被输出为文本成为 solidity文件的一部分。m是一个全局int类型，
每执行一次循环，就会自增，于是每次循环打印出来的语句都代表不同的结构体变量。这样，便初步解决了如何生成solidity语言的buchi自动机监控器的问题。