UPPAAL命令行跑SMC；命令行运行SMC；命令行SMC； :::success

  1. 本文基于uppaal-4.1.25版本，Win10 20H2。
  2. 如果不清楚如何写SMC性质语句，请阅读SMC问题总结。 :::

    一、基本命令行语法

    Win10利用power shell跑UPPAAL：
    首先进入\uppaal\bin-Windows目录，把要验证的.xml模型拷贝到该目录，然后按下shift+鼠标右键打开power shell（或者其他命令行），然后运行
    .\verifyta.exe [OPTION]... MODEL QUERY, where MODEL is a model file and QUERY is a query file.
    其中QUERY会验证写在xml文件中的所有验证语句。具体查看本文末的help文档。

    二、Example

    这里提供最常用的两个例子，批量运行可以使用python调用系统命令行，并且可以利用多线程来加快运行速度。文档链接：python 多线程。 :::success 注意：在命令行中，UPPAAL会对所有语句进行验证，无法指定某个语句。 :::

    1. 运行simulate，并保存观测结果

    写好验证性质以后，直接在命令行输入.\verifyta.exe .\模型名字 > 输出文件名即可。
    比如.\verifyta.exe .\NPN_Initial.xml > result.txt即可将运行结果输出到result.txt文件中。

  • 提示1：使用> result.txt会让结果不再显示到命令行中，可以用cat result.txt来输出结果。

    也可以用分号;将两个语句连起来：

    1. .\verifyta.exe .\NPN_Initial.xml > result.txt ; cat result.txt

  • 提示2：可以通过加-r [ --seed ] arg来指定随机数帮助复现结果。否则默认是当前时间：

    1. .\verifyta.exe -r 0 .\NPN_Initial.xml > result.txt ; cat result.txt

    输出结果分析

    验证语句为simulate [<=10000;1000] {Output.pass}，为了节约篇幅，下面只贴了输出的一部分。 ```powershell Options for the verification: Generating no trace Search order is breadth first Using conservative space optimisation Seed is 0 State space representation uses minimal constraint systems  Verifying formula 1 at /nta/queries/query1/formula  — Formula is satisfied. Output.pass:

……

……

……

  1. 从运行的结果来看，每行的开头为验证次数，后面的二维数第0个元素为时刻横坐标，后面元素为对应的观测纵坐标。从结果中还可以注意到，虽然验证语句中限制了时间`<=10000`，但实际运行时仍会超出20%-50%的时间。
  2. <a name="SzLk3"></a>
  3. ## 2. 运行simulate并保存所需trace
  4. 在运行`simulate [<=10000; 1000] {Output.pass}`时，有时候我们需要保存`Output.pass==1`的Trace。虽然这条语句模拟了1000次，但是在Get Trace的时候只能获取某一个Trace，而这个Trace不一定是我们需求的。
  5. <a name="dmtRh"></a>
  6. ### 思路
  7. 多次运行`simulate [<=10000; 1] {Output.pass}`，当出现`Output.pass==1`的观测时，保存本次的Trace。
  8. <a name="T7W4a"></a>
  9. ### 命令行
  10. 在写好性质以后，在命令行输入以下内容可以运行并保存模拟的Trace。为了判断模拟结果是否符合要求，进而判断我们是否需要保存该Trace，我们开发了一套python工具`uppaal-controller包`来辅助检测。
  11. <a name="E8Mmp"></a>
  12. ## 3. 运行Pr[<=T] (<>psi)，并显示观测结果
  13. 写好验证性质以后，直接在命令行输入`.\verifyta.exe .\模型名字`即可，如果需要保存输出请看[1](#JI9cT)。
  14. :::danger
  15. **注意：**在运行该语句时，不建议添加`-r`来指定随机数，因为多次验证结果为<br />`[0, 0.0981446]`（不可能）的情况下，仍有可能出现`[0.0169465, 0.116203]`（有可能）的结果。
  16. :::
  17. 相关参数设置：
  18. ```powershell
  19. SMC:
  20.   -r [ --seed ] arg                    Set seed for random number generator
  21.                                        (default is current time).
  22.   -p [ --lower-delta ] arg             lower (delta) probabilistic uncertainty.
  23.   -P [ --upper-delta ] arg             upper (delta) probabilistic uncertainty.
  24.   -a [ --alpha ] arg                   probability of false negatives (alpha).
  25.   -B [ --beta ] arg                    probability of false positives (beta).
  26.   -E [ --epsilon ] arg                 probability uncertainty (epsilon).
  27.   -i [ --u0 ] arg                      threshold u0 for comparing
  28.                                        probabilities.
  29.   -j [ --u1 ] arg                      threshold u1 for comparing
  30.                                        probabilities.
  31.   -w [ --histogram-bar-width ] arg     width of buckets in histogram. Should
  32.                                        not be set in conjunction with
  33.                                        --histogram-bar-count
  34.   --histogram-bar-count arg            number of buckets in histogram. Should
  35.                                        not be set in conjunction with
  36.                                        --histogram-bar-width
  37.   -c [ --parametric-comp ] arg         <0|1>
  38.                                        activate (1) or not (0) the SMC
  39.                                        parametric comparison.
  40.   -V [ --smc-coverage ]                activate SMC coverage.
  41.   -R [ --resolution ] arg              simulation resolution (pixels).
  42.   -D [ --discretization ] arg          discretization step size (time) for
  43.                                        hybrid systems.
  44.   -L [ --probability-log ] arg         SMC-Log file.
  45.   -F [ --sampling-time ] arg           outputs to a file a sampling of
  46.                                        simulations (when simulate is used).

三、官方Help文档

双击打开verifyta.exe会告诉如何查看help。

  1. Usage: D:\uppaal64-4.1.25-5\bin-Windows\verifyta.exe [OPTION]... MODEL QUERY
  2. where MODEL is a model file and QUERY is a query file.
  3. If QUERY is missing it will be guessed.
  4. Options:
  5.   -h [ --help ]                        produce help message
  7. General:
  8.   -H [ --hashtable-size ] arg          Set hash table size for bit state
  9.                                        hashing to 2**n bits
  10.                                        (default = 27)
  11.   -n [ --extrapolation ] arg           <0|1|2|3|4>
  12.                                        Select extrapolation operator.
  13.                                          0: Automatic
  14.                                          1: No extrapolation (use with care)
  15.                                          2: Difference extrapolation
  16.                                          3: Location based extrapolation
  17.                                          4: Lower/upper extrapolation
  19.   -t [ --diagnostic ] arg              <0|1|2>
  20.                                          Generate diagnostic information on
  21.                                        stderr.
  22.                                            0: Some trace
  23.                                            1: Shortest trace (disables reuse)
  24.                                            2: Fastest trace (disables reuse)
  25.   -o [ --search-order ] arg            <0|1|2|3|4>
  26.                                        Select search order.  Only 0 and 1 for
  27.                                        TIGA properties.
  28.                                          0: Breadth first (short-hand -b)
  29.                                          1: Depth first (short-hand -d)
  30.                                          2: Random depth first
  31.                                          3: Optimal first (requires -t1 or -t2)
  32.                                          4: Random optimal depth first
  33.                                        (requires -t1 or -t2)
  35.   --state-representation arg           <0|1|2|3>
  36.                                        Choose how discrete states should be
  37.                                        represented. (default 1)
  38.                                         0: Difference Bound Matrix. Has
  39.                                            short-hand -C
  40.                                         1: Compact DBM. Uses less space but
  41.                                            more time compared to pure DBM.
  42.                                         2: Bit-state hashing.
  43.                                            Under-approximates states. Has
  44.                                            short-hand -Z.
  45.                                         3: Convex-hull approximation.
  46.                                            Over-approximates states. Has
  47.                                            short-hand -A.
  48.   -S [ --statespace-consumption ] arg  <0|1|2|3>
  49.                                           Optimize space consumption (0 = none,
  50.                                        1 = default, 2 = aggressive, 3 =
  51.                                        extreme)
  52.   -T [ --reuse-statespace ]            Reuse state space when several
  53.                                        properties are examined.
  54.   -N [ --polyhedra ]                   Use polyhedra verification of
  55.                                        stopwatches over-approximation
  56.   -M [ --modest ]                      activate Modest semantics for updates.
  58. Output:
  59.   -f [ --prefix ] arg                  Write symbolic traces to files
  60.                                        'prefix-n.xtr' rather than to stderr.
  61.   -W                                   Disable warnings
  62.   -y [ --post-symbolic ]               Display traces symbolically
  63.                                        (post-stable).
  64.   -Y [ --pre-symbolic ]                Display traces symbolically (pre- and
  65.                                        post-stable).
  66.   -q [ --nosummary ]                   Do not display the option summary.
  67.   -x [ --save-system ] arg             Save the (modified) system in XML
  68.                                        format, in specified file.
  69.                                        If the system has been modified, an
  70.                                        associated query file is created.
  71.   -X [ --save-trace ] arg              Save the symbolic trace in file
  72.                                        '<arg>Propertynumber.xml'
  73.   -O [ --simulation-format ] arg       write the filtered simulation
  74.                                        trajectories to:
  75.                                        std: one trajectory per line into
  76.                                             standard output (default)
  77.                                        csv: one trajectory per file in
  78.                                             comma-separated-values format.
  80. Miscellaneous:
  81.   -s [ --silence-progress ]            Do not display the progress indicator.
  82.   -u [ --summary ]                     Show verification summary at the end
  83.                                        (incorrect for liveness properties).
  84.   -v [ --version ]                     Show version number.
  86. SMC:
  87.   -r [ --seed ] arg                    Set seed for random number generator
  88.                                        (default is current time).
  89.   -p [ --lower-delta ] arg             lower (delta) probabilistic uncertainty.
  90.   -P [ --upper-delta ] arg             upper (delta) probabilistic uncertainty.
  91.   -a [ --alpha ] arg                   probability of false negatives (alpha).
  92.   -B [ --beta ] arg                    probability of false positives (beta).
  93.   -E [ --epsilon ] arg                 probability uncertainty (epsilon).
  94.   -i [ --u0 ] arg                      threshold u0 for comparing
  95.                                        probabilities.
  96.   -j [ --u1 ] arg                      threshold u1 for comparing
  97.                                        probabilities.
  98.   -w [ --histogram-bar-width ] arg     width of buckets in histogram. Should
  99.                                        not be set in conjunction with
  100.                                        --histogram-bar-count
  101.   --histogram-bar-count arg            number of buckets in histogram. Should
  102.                                        not be set in conjunction with
  103.                                        --histogram-bar-width
  104.   -c [ --parametric-comp ] arg         <0|1>
  105.                                        activate (1) or not (0) the SMC
  106.                                        parametric comparison.
  107.   -V [ --smc-coverage ]                activate SMC coverage.
  108.   -R [ --resolution ] arg              simulation resolution (pixels).
  109.   -D [ --discretization ] arg          discretization step size (time) for
  110.                                        hybrid systems.
  111.   -L [ --probability-log ] arg         SMC-Log file.
  112.   -F [ --sampling-time ] arg           outputs to a file a sampling of
  113.                                        simulations (when simulate is used).
  115. The ordering of options is significant.
  117. Environment variables:
  118.   UPPAAL_DUMP_STATE          output a state satisfying the property.
  119.   UPPAAL_DISABLE_SWEEPLINE   disable sweepline method
  120.   UPPAAL_DISABLE_OPTIMISER   disable peephole optimiser
  121.   UPPAAL_DISABLE_SYMMETRY    disable symmetry reduction
  122.   UPPAAL_COMPILE_ONLY        write compiled model to stdout and stop
  123.   UPPAAL_OLD_SYNTAX          use UPPAAL 3.4 syntax
  125. The value of these variables does not matter. Defining them is
  126. enough to activate the feature in question.