This commit is contained in:
Amaury Chamayou 2024-04-19 14:40:06 +01:00 коммит произвёл GitHub
Родитель a6131dd37a
Коммит fe19966a72
Не найден ключ, соответствующий данной подписи
Идентификатор ключа GPG: B5690EEEBB952194
1 изменённых файлов: 4 добавлений и 4 удалений

Просмотреть файл

@ -10,16 +10,16 @@ SPECIFICATION
POSTCONDITION
TraceMatchedNonTrivially
\* Some of the traces in TraceSpec may not refine the high-level specification ccfraft.
\* Some of the traces in TraceSpec may not refine the high-level specification MultiNodeReads.
\* Those traces will cause the trace validator to report a counterexample even if
\* TraceSpec contains a trace that refines ccfraft and fully matches the log file.
\* The real property to check is that TraceSpec contains a trace that refines ccfraft and
\* TraceSpec contains a trace that refines MultiNodeReads and fully matches the log file.
\* The real property to check is that TraceSpec contains a trace that refines MultiNodeReads and
\* matches the full log. However, TLA cannot check this property directly because it
\* is a hyperproperty.
PROPERTIES
MNRSpec
\* TLA has only limited support for hyperproperties. The following property is a poorman's
\* TLA has only limited support for hyperproperties. The following property is a poor man's
\* hyperproperty that asserts that TLC generated *at least one* trace that fully matches the
\* log file.
PROPERTIES