Molly 安装与测试

Molly下载地址:https://github.com/palvaro/molly

首先阅读tutorial.md文件,安装方法按照Installation.md来执行;

需要注意点:

  1. 在mac OS下不能使用brew install来安装apr、apr-util,需要下载这两个组件的源码,通过make、install的方式进行安装;
  2. bin 目录下只有c4,缺少z3的安装文件,需要自己下载安装;
  3. 依赖安装完毕后,需要将依赖的库添加到PATH中;

安装Scala构建工具:sbt

brew install sbt@1

参考:http://www.scala-sbt.org/download.html

原因是Molly是采用scala语言编写;

Apr下载与安装:

https://apr.apache.org/download.cgi
https://gist.github.com/zedshaw/4e14bbca46eb21aad08d

apr-util:

https://apr.apache.org/download.cgi
http://mac-dev-env.patrickbougie.com/apr-util/

c4安装指南:

https://github.com/bloom-lang/c4/tree/1e9b8fd8bf7c11004b21e12945eb30b2c1818e6a

依赖安装

C4依赖了flex , bison, cmake, apr ,
apr-util and SQLite

brew install flex
brew install bison
brew install cmake
brew install SQLite
#.bash_profile 中添加
export PATH="/usr/local/apr/bin:$PATH"
export PATH="/usr/local/apr-util/bin:$PATH"
export PATH="/usr/local/opt/bison/bin:$PATH"
export PATH="/usr/local/opt/sqlite/bin:$PATH"
export PATH="/usr/local/opt/flex/bin:$PATH"
c4安装
mkdir build
cd build
cmake ..
make

下载z3:

下载地址:https://github.com/Z3Prover/z3

安装命令:

python scripts/mk_make.py
cd build
make
sudo make install

z3 是微软开源的一款定理求解器;

环境安装时遇到的问题:

  • unresolved dependency
sbt.ResolveException: unresolved dependency:

解决方案:
删除 ~/.ivy2/cache目录下的对应的文件目录,重新执行命令;

  • 安装c4时,出现错误中断
APR_CONFIG_EXECUTABLE-NOTFOUND

表示APR依赖安装的不正确,找不到具体的包,请检查apr是否通过源码编译的方式安装成功;

用例执行:

  • 无反例的示例执行:
sbt "run-main edu.berkeley.cs.boom.molly.SyncFTChecker -N a,b,c -t 5 -f 0 --prov-diagrams demo_v1.ded"
  • 有反例的示例执行:
sbt "run-main edu.berkeley.cs.boom.molly.SyncFTChecker \
    src/test/resources/examples_ft/delivery/simplog.ded \
    src/test/resources/examples_ft/delivery/deliv_assert.ded \
    --EOT 4 \
    --EFF 2 \
    --nodes a,b,c \
    --crashes 0 \
    --prov-diagrams"
  • 图形化查看结果: 在生成output目录中运行httpServer,通过访问localhost:8080来查看执行路径;
python -m SimpleHTTPServer 8080

 

Advertisements

发表评论

Fill in your details below or click an icon to log in:

WordPress.com 徽标

You are commenting using your WordPress.com account. Log Out /  更改 )

Google photo

You are commenting using your Google account. Log Out /  更改 )

Twitter picture

You are commenting using your Twitter account. Log Out /  更改 )

Facebook photo

You are commenting using your Facebook account. Log Out /  更改 )

Connecting to %s