TLA +: временные свойства не проверяются - PullRequest
Новая
       15

TLA +: временные свойства не проверяются

0 голосов
/ 11 марта 2019

У меня есть этот игрушечный пример, и по какой-то причине ни одно из временных свойств никогда не утверждается.Даже такие нелепые, как [](h = 123456), не подводят TLC.Что я не понимаю?

intro.tla 

----------------------------------------------------- MODULE intro -----------------------------------------------------

EXTENDS Naturals

VARIABLE h

Init == h \in 1..12

Invariants == h \in 1..12

Next == h' = (h%12) + 1

Spec ==
 /\ Init
 /\ [][Next]_h
 \* None of these cause the model checker to fail
 /\ (\A i \in 1..15 : []<>(h = i))
 /\ []<>(h = 123456)
 /\ [](h = 123456)
 /\ <>(h = 123456)
 /\ [](FALSE)

THEOREM Spec => []Invariants

=======================================================================================================================

intro.cfg 

SPECIFICATION Spec
INVARIANTS Invariants

tlc intro 

TLC2 Version 2.13 of 18 July 2018 (rev: bfdbe00)
Running breadth-first search Model-Checking with seed -1431825986697619670 with 8 workers on 8 cores with 7131MB heap and 64MB offheap memory (Linux 5.0.0-arch1-1-ARCH amd64, Oracle Corporation 1.8.0_202 x86_64).
Parsing file /home/golly/projects/private/talks-wip/tla/intro.tla
Parsing file /tmp/Naturals.tla
Semantic processing of module Naturals
Semantic processing of module intro
Starting... (2019-03-11 12:20:09)
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Finished computing initial states: 12 distinct states generated.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 7.8E-18
  based on the actual fingerprints:  val = 1.6E-18
24 states generated, 12 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 0.
The average outdegree of the complete state graph is 0 (minimum is 0, the maximum 0 and the 95th percentile is 0).
Finished in 00s at (2019-03-11 12:20:09)

1 Ответ

0 голосов
/ 13 марта 2019

Характеристики поведения состоят из начального состояния (Init) и формулы следующего состояния ([][Next]_h). Я считаю, что здесь происходит то, что IDE или TLC видят этих двоих и игнорируют остальных. Как и должно быть: эти дополнительные пункты не заставляют поведение нарушать ваши свойства: они просто говорят, что начальных состояний и действий меньше, чем вы думали. Если вы хотите сделать их свойствами вашей спецификации, добавьте эти пункты к Properties в панели инструментов.

...