ctrl+shift+p filters: :st2 :st3 :win :osx :linux
浏览

Clafer 工具

作者 gsdlab 全部

将 Clafer 编译器和实例生成器集成到 Sublime Text 2/3 中

标签 Clafer， 编译器， 实例生成器

详细信息

  • 2017.06.28.18.43.11
  • github.​com
  • github.​com
  • 7 年前
  • 2 小时前
  • 10 年前

安装次数

  • 总数 212
  • Win 112
  • Mac 57
  • Linux 43
8月6日 8月5日 8月4日 8月3日 8月2日 8月1日 7月31日 7月30日 7月29日 7月28日 7月27日 7月26日 7月25日 7月24日 7月23日 7月22日 7月21日 7月20日 7月19日 7月18日 7月17日 7月16日 7月15日 7月14日 7月13日 7月12日 7月11日 7月10日 7月9日 7月8日 7月7日 7月6日 7月5日 7月4日 7月3日 7月2日 7月1日 6月30日 6月29日 6月28日 6月27日 6月26日 6月25日 6月24日 6月23日
Windows 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
Mac 1 1 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
Linux 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

读取 me.txt

源代码
raw.​githubusercontent.​com

Clafer 工具

v0.4.5

将 Clafer 编译器和实例生成器 集成到 Sublime Text 2/3。

查看 Clafer 0.4.5 的发行说明。

贡献者

特点和用法

  • 关键词、运算符、注释以及整数和字符串常量的语法高亮
  • 编译和验证 <CTRL>+b。要更改命令的参数，请选择“首选项”->“浏览包” -> “ Clafer Tools ” -> 编辑 Clafer.sublime-build
    • 首选项 -> 浏览包
    • cd Clafer Tools
    • 编辑 Clafer.sublime-build
  • 使用以下方式生成实例（带有简单的范围推断）
    • 基于 Alloy 的实例生成器 <CTRL>+i, g, a
    • 基于 Choco 的实例生成器 <CTRL>+i, g, c
    • 基于 Z3 SMT 的实例生成器 <CTRL>+i, g, s（仅适用于 0.3.6.1）

安装

  1. 安装 Sublime Text 3。在 Ubuntu 上，通过执行 sudo apt install sublime-text-installer 来自 WebUpd8 PPA 安装。
  2. 在 Sublime Text 中
    • 安装 Package Control
      • 工具 -> 安装 Package Control...
    • 安装包 SublimeREPL， Clafer Tools 和（可选） SidebarEnhancements
      • 首选项 -> Package Control -> 安装包
      • 输入包名称
    • 打开 Packages 文件夹
      • 首选项 -> 浏览包...
      • 将 Clafer Tools 中的 SublimeREPL 文件夹从 Clafer Tools 复制到 Packages
        • 在 Mac 上，使用 合并 选项而不是 替换 选项
  3. 下载 Clafer Tools 的最新二进制发行版本
    • Clafer 工具
    • 将 clafer-tools-0.4.5 文件夹的内容解压到 Packages/Clafer-Bin
      • 确保文件夹结构不是 Packages/Clafer-Bin/clafer-tools-0.4.5，即 clafer-tools-0.4.5 文件夹的内容直接位于 Clafer-Bin 内部
    • （可选）将 Clafer-Bin 添加到变量 PATH 中。
  4. 仅适用于 Windows
    • 基于合金的实例生成器仅在Windows上的32位Java上工作，如果您只有64位Java安装，您会看到一个错误： Exception in thread "main" java.lang.UnsatisfiedLinkError: no minisatproverx1 in java.library.path。

已知的限制和解决方案

  • 在Windows上 - 将PATH设置为32位Java安装

    • 安装 32位JDK 但不要修改PATH指向它（不再有32位JRE）
    • 在Sublime Text中
      • 首选项 -> 包设置 -> SublimeREPL -> 设置 - 默认
      • 将 default_extended_env 设置为 "default_extend_env": {"PATH": "C:/Program Files (x86)/Java/jdk1.8.0_102/bin;{PATH}"},

  • 在Linux和Mac上

    • Python 3可执行文件称为 python3，最佳解决方案是创建一个名为 python 的符号链接，指向 /usr/bin/python3
      • 在 Packages/Clafer Tools 中执行 ln -s /usr/bin/python3 python。
    • 还需要将当前目录 . 添加到 PATH 中，以便找到可执行文件。在您的 .profile 末尾添加以下行
      • PATH=".:$PATH"
    • 为了能让python找到 Z3 库，在您的 .profile 中添加以下行
      • 在Linux上，export LD_LIBRARY_PATH="~/.config/sublime-text-3/Packages/Clafer-Bin:$LD_LIBRARY_PATH"
      • 在Mac上，export DYLD_LIBRARY_PATH="~/.config/sublime-text-3/Packages/Clafer-Bin:$DYLD_LIBRARY_PATH"

  • 在MacOS Yosemite上，设置变量 PATH 的首选方法是编辑 /etc/paths。然而，尽管如此，Sublime Text 2/3 仍然不会看到指定的值，因为它是一个GUI应用程序，并且它只会看到 /usr/bin:/bin:/usr/sbin:/sbin:/。要检查Sublime visibile的 PATH 的值

    1. 打开控制台 视图 -> 显示控制台
    2. 执行 import os; print (os.environ['PATH'])
    3. 如果您看到 /usr/bin:/bin:/usr/sbin:/sbin:/，您会受到Yosemite PATH 错误的影响，并且 ClaferChocoIG 将无法为您完成模型，因为它调用 clafer可执行文件。
    4. 解决方法是
      • 创建一个符号链接 sudo ln -s ~/Library/Application\ Support/Sublime\ Text\ 3/Packages/Clafer-Bin/clafer /usr/bin/clafer，这样 clafer 可执行文件就会在默认的 PATH 上可见。
    5. 为了方便使用ClaferChocoIG，通过执行 sudo mv ~/Library ApplicationUser\u0020Support/Sublime\u0020Text\ 3/Packages/Clafer-Bin/claferchocoig.sh /usr/bin 将脚本 claferchocoig.sh（包含在Mac二进制发行版中）移动到 /usr/bin。

  • ClaferSMT在Clafer Tools 0.3.6.1的二进制版本中依赖于Python包 bintrees，要在Windows上安装，请执行 pip install bintrees，在Linux和Mac上执行 pip3 install bintrees。

计划改进

  • 量词表达式（如 [ all disj x1; x2 : X | ... ]）的代码片段