FDR使用说明简介.doc

FDR使用说明简介 安装 从 下载FDR2软件包 将FDR2软件包解压到“/opt”目录下 设置环境变量FDRHOME: 编辑.bashrc文件，在该文件中加入下列内容： FDRHOME=/opt/fdr-2.83-linux-academic 编辑.bash_profile 文件，将PATH环境变量修改如下： PATH=$PATH:$HOME/bin:$FDRHOME 然后在语句“export PATH”下面加上“export FDRHOME” 最后在终端运行以下命令： Source .bash_profile Reboot 运行FDR2 系统重启后将当前目录改为“/opt/fdr-2.83-linux-academic/bin”，然后在终端运行fdr2文件，随后显示FDR2系统界面如下： 图1 FDR2主窗口简介： FDR2的主窗口如图2所示： 图2 FDR2的主窗口从上至下由五部分组成，分别是： 菜单栏 该部分位于窗口的最上边一栏（如图3所示）。其中File下拉菜单中提供了文 图3 件的加载（Load）、重载（Re-load）、编辑（Edit）、退去（Exit）以及运行所有命题检测的命令All Asserts。Assert下拉菜单中提供对选定命题检测运行命令（Run）和调试命令（Debug）。Process下拉菜单中提供了根据进程列表（Process List）在命题列表（Assertion List）中生成相应的死锁、活锁、确定性命题的命令Deadlock、LiveLock、Deterministic。Options下拉菜单中提供以下五个命令：.Supercompilation、Bisimulate leaves、Messages、Compact、Examples per check、Show status、Restart（这几个命令使用方法请参考fdr2manual.pdf）。Interrupt按钮提供了中止当前的检测或编译并使FDR立即执行将来的命令。Help按钮用于提供帮助信息。 Tab Bar 该部分位于菜单栏之下（如图4所示）。这部分包含了FDR可以执行的不同 图4 检测的标签，如Refinement、Deadlock、Livelock、Dererminism。此外还有一个可以与编译器和任意表达式评价的交互标签Evaluate。 Tab Pane 该部分位于Tab Bar的下面，主窗口的中间（如图5所示）。该部分用来 图5 输入与当前标签（tab）有关的信息。这可以用于建立精化语句或评估表达式。在简单的精化中左边的进程选择器Specification用于选择描述进程，中间的Model用于选择精化模型（有Trace、Failures、Failures-divergence三种模型），右边的选择器Implementation用于选择实现进程。当选择完这三项后点击Check按钮在Assertion List中将生成一个检测过的命题（句子前打‘√’或‘×’或‘×.’），点击Add按钮在Assertion List中将生成一个没有检测过的命题（命题前打‘？’），点击Clear将消除Specification和Implementation选择前中的进程。 Assertion List 该部分是主窗口中最重要的一部分，位于Tab Pane下（如图6所示）。 图6 该部分包含由列举了有关进程精化、死锁或活锁有无、或其他模型属性的命题。对于每个句子，FDR是否正确（句子前打‘√’）、错误（句子前打‘×’或‘×.’）、没测试（句子前打‘？’）或正在测试（句子前有个钟表符号）。当一个文件加载进来，该脚本文件中所描述的所有精化属性都被列举咋Assertion List中且前面都加问号。当需要是还可以从Tab Pane中向Assertion List中加入属性（如Tab Pane中所述）。可以双击加问号的属性，然后FDR会自动对它测试，或者点击File中All Asserts命令可以对Assertion List中所有属性进行测试。 Process List 该部分位于主窗口的最下面，也即Assertion List的下边（如图7所示）。