关键字：uppaal命令行，命令行验证 :::success 本文基于uppaal-4.1.25版本，Win10 20H2。 ::: 利用命令行来运行UPPAAL的验证过程，设置相关参数（结果返回最短、最快，搜索模式深度、广度优先等），并输出相应结果。

一、基本语法

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. 保存xtr格式的Trace

跑一个验证并返回结果（-t），并保存xtr格式的trace（-f）。

  1. .\verifyta.exe -t 1 -f traceFileName .\xmlModelFile.xml
  3. #############################################################################
  5. -t [ --diagnostic ] arg      <0|1|2> Generate diagnostic information on stderr.
  6.                                   0: Some trace
  7.                                   1: Shortest trace (disables reuse)
  8.                                   2: Fastest trace (disables reuse)
  10. -f [ --prefix ] arg          Write symbolic traces to files 'prefix-n.xtr' 
  11.                                                          rather than to stderr.
  • traceFileName是保存的反例文件，不需要加.xtr；
  • 注意，必须有-t，不然不能输出结果；

    2. 保存xml格式的Trace

    跑一个验证并返回验证结果（-t），并保存xml格式的trace（-X）。 ```powershell .\verifyta.exe -t 1 -X readableTraceFileName .\xmlModelFile.xml
#

-t [ —diagnostic ] arg <0|1|2> Generate diagnostic information on stderr. 0: Some trace 1: Shortest trace (disables reuse) 2: Fastest trace (disables reuse)

-X [ —save-trace ] arg Save the symbolic trace in file ‘Propertynumber.xml’

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