UPPAAL命令行

Posted 2021-09-07 DreaMing

UPPAAL命令行操作

UPPAAL版本：uppaal64-4.1.25

一、基本用法

windows下CMD跑UPPAAL：

首先进入\\uppaal\\bin-Windows目录，把要验证的.xml模型拷贝到该目录，然后按下shift+鼠标右键打开powershell（或者其他命令行），然后运行

.\\verifyta.exe [OPTION]... MODEL QUERY,
where MODEL is a model file and QUERY is a query file.

其中QUERY会验证写在xml文件中的所有验证语句。具体查看help文档。

二、Example

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

   .\\verifyta.exe -t 1 -f traceFileName .\\xmlModelFile.xml

   • traceFileName不需要加.xtr。
   • 注意，必须有-t，不然不能输出结果。

   • 提示：可以通过加-r arg来指定随机数。否则默认是当前时间。

     • .\\verifyta.exe -r 0 -t 1 -f traceFileName .\\xmlModelFile.xml

2. 跑一个验证并返回验证结果（-t），保存xml格式的trace（-X）

   .\\verifyta.exe -t 1 -X readableTraceFileName .\\xmlModelFile.xml

   • readableTraceFileName不需要加.xml
   • 注意，必须有-t，不然不能输出结果。
   • 注意，-X和-f好像不能同时使用
   • 提示：可以通过加-r arg来指定随机数。
   • xml在线格式化 | 菜鸟工具

三、官方Help文档

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

Usage: D:\\uppaal64-4.1.25-5\\bin-Windows\\verifyta.exe [OPTION]... MODEL QUERY
where MODEL is a model file and QUERY is a query file.
If QUERY is missing it will be guessed.
Options:
  -h [ --help ]                        produce help message

General:
  -H [ --hashtable-size ] arg          Set hash table size for bit state
                                       hashing to 2**n bits
                                       (default = 27)
  -n [ --extrapolation ] arg           <0|1|2|3|4>
                                       Select extrapolation operator.
                                         0: Automatic
                                         1: No extrapolation (use with care)
                                         2: Difference extrapolation
                                         3: Location based extrapolation
                                         4: Lower/upper extrapolation

  -t [ --diagnostic ] arg              <0|1|2>
                                         Generate diagnostic information on
                                       stderr.
                                           0: Some trace
                                           1: Shortest trace (disables reuse)
                                           2: Fastest trace (disables reuse)
  -o [ --search-order ] arg            <0|1|2|3|4>
                                       Select search order.  Only 0 and 1 for
                                       TIGA properties.
                                         0: Breadth first (short-hand -b)
                                         1: Depth first (short-hand -d)
                                         2: Random depth first
                                         3: Optimal first (requires -t1 or -t2)
                                         4: Random optimal depth first
                                       (requires -t1 or -t2)

  --state-representation arg           <0|1|2|3>
                                       Choose how discrete states should be
                                       represented. (default 1)
                                        0: Difference Bound Matrix. Has
                                           short-hand -C
                                        1: Compact DBM. Uses less space but
                                           more time compared to pure DBM.
                                        2: Bit-state hashing.
                                           Under-approximates states. Has
                                           short-hand -Z.
                                        3: Convex-hull approximation.
                                           Over-approximates states. Has
                                           short-hand -A.
  -S [ --statespace-consumption ] arg  <0|1|2|3>
                                          Optimize space consumption (0 = none,
                                       1 = default, 2 = aggressive, 3 =
                                       extreme)
  -T [ --reuse-statespace ]            Reuse state space when several
                                       properties are examined.
  -N [ --polyhedra ]                   Use polyhedra verification of
                                       stopwatches over-approximation
  -M [ --modest ]                      activate Modest semantics for updates.

Output:
  -f [ --prefix ] arg                  Write symbolic traces to files
                                       \'prefix-n.xtr\' rather than to stderr.
  -W                                   Disable warnings
  -y [ --post-symbolic ]               Display traces symbolically
                                       (post-stable).
  -Y [ --pre-symbolic ]                Display traces symbolically (pre- and
                                       post-stable).
  -q [ --nosummary ]                   Do not display the option summary.
  -x [ --save-system ] arg             Save the (modified) system in XML
                                       format, in specified file.
                                       If the system has been modified, an
                                       associated query file is created.
  -X [ --save-trace ] arg              Save the symbolic trace in file
                                       \'<arg>Propertynumber.xml\'
  -O [ --simulation-format ] arg       write the filtered simulation
                                       trajectories to:
                                       std: one trajectory per line into
                                            standard output (default)
                                       csv: one trajectory per file in
                                            comma-separated-values format.

Miscellaneous:
  -s [ --silence-progress ]            Do not display the progress indicator.
  -u [ --summary ]                     Show verification summary at the end
                                       (incorrect for liveness properties).
  -v [ --version ]                     Show version number.

SMC:
  -r [ --seed ] arg                    Set seed for random number generator
                                       (default is current time).
  -p [ --lower-delta ] arg             lower (delta) probabilistic uncertainty.
  -P [ --upper-delta ] arg             upper (delta) probabilistic uncertainty.
  -a [ --alpha ] arg                   probability of false negatives (alpha).
  -B [ --beta ] arg                    probability of false positives (beta).
  -E [ --epsilon ] arg                 probability uncertainty (epsilon).
  -i [ --u0 ] arg                      threshold u0 for comparing
                                       probabilities.
  -j [ --u1 ] arg                      threshold u1 for comparing
                                       probabilities.
  -w [ --histogram-bar-width ] arg     width of buckets in histogram. Should
                                       not be set in conjunction with
                                       --histogram-bar-count
  --histogram-bar-count arg            number of buckets in histogram. Should
                                       not be set in conjunction with
                                       --histogram-bar-width
  -c [ --parametric-comp ] arg         <0|1>
                                       activate (1) or not (0) the SMC
                                       parametric comparison.
  -V [ --smc-coverage ]                activate SMC coverage.
  -R [ --resolution ] arg              simulation resolution (pixels).
  -D [ --discretization ] arg          discretization step size (time) for
                                       hybrid systems.
  -L [ --probability-log ] arg         SMC-Log file.
  -F [ --sampling-time ] arg           outputs to a file a sampling of
                                       simulations (when simulate is used).

The ordering of options is significant.

Environment variables:
  UPPAAL_DUMP_STATE          output a state satisfying the property.
  UPPAAL_DISABLE_SWEEPLINE   disable sweepline method
  UPPAAL_DISABLE_OPTIMISER   disable peephole optimiser
  UPPAAL_DISABLE_SYMMETRY    disable symmetry reduction
  UPPAAL_COMPILE_ONLY        write compiled model to stdout and stop
  UPPAAL_OLD_SYNTAX          use UPPAAL 3.4 syntax

The value of these variables does not matter. Defining them is
enough to activate the feature in question.