zoukankan      html  css  js  c++  java
  • 用C++生成solidity语言描述的buchi自动机的初级经验

    我的项目rvtool(https://github.com/Zeraka/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_label_0.next_state = 0;
    
            ws_0.word = "!event3";
            ws_0.wordset["event3"] = 0;
            monitor_label_0.word_sets.push(ws_0);
    
            monitor_state_0.monitor_labels.push(monitor_label_0);
    
            monitor_label_1.label = "event3";
            monitor_label_1.next_state = 1;
    
            ws_1.word = "event3";
            ws_1.wordset["event3"] = 1;
            monitor_label_1.word_sets.push(ws_1);
    
            monitor_state_0.monitor_labels.push(monitor_label_1);
            monitor_state_0.label_numbers = 2;
            monitor.nodes[0] = monitor_state_0;
            //=================
    
            monitor_state_1.own_state = 1;
    
            monitor_label_2.label = "!event1 & !event3 & event4";
            monitor_label_2.next_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_state_1.monitor_labels.push(monitor_label_2);
            monitor_state_1.label_numbers = 1;
            monitor.nodes[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<<";
    ";
            m++;
        }
    

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

  • 相关阅读:
    爱普生L4168打印出来是白纸,复印OK,打印机测试也OK 解决方案
    json序列化对象
    "割裂"的西安
    资金投资心得
    【练内功,促成长】算法学习(3) 二分查找
    在ReactNative中实现Portal
    node创建GIT分支,并修改代码提交
    关于"三分钟热度"问题的思考
    参考vue-cli实现自己的命令行工具(demo)
    【练内功,促成长】算法学习(2) 排序算法
  • 原文地址:https://www.cnblogs.com/goto2091/p/13620635.html
Copyright © 2011-2022 走看看