PSL/A Practical Introduction to PSL/Basic Temporal Properties/ru — различия между версиями
ANA (обсуждение | вклад) (Новая страница: «{{PSL TOC}} ==Basic Temporal Properties While== While the Boolean layer consists of Boolean expressions that hold or do not hold at a given cycle, the temporal l…») |
Valentin (обсуждение | вклад) (→Basic Temporal Properties While) |
||
| Строка 1: | Строка 1: | ||
{{PSL TOC}} | {{PSL TOC}} | ||
| − | == | + | ==Основные временные свойства While== |
| + | <!-- | ||
While the Boolean layer consists of Boolean expressions that hold or do not | While the Boolean layer consists of Boolean expressions that hold or do not | ||
hold at a given cycle, the temporal layer provides a way to describe relationships | hold at a given cycle, the temporal layer provides a way to describe relationships | ||
| Строка 11: | Строка 12: | ||
a should hold at the first cycle and at every cycle following the first cycle – | a should hold at the first cycle and at every cycle following the first cycle – | ||
that is, at every cycle. | that is, at every cycle. | ||
| + | --> | ||
| + | В то время как Булевый слой состоит из Булевых выражений, которые выполняются или не выполняются в данном цикле, временной слой предоставляет путь для описания взаимоотношений между Булевыми выражениями по времени. PSL утверждение обычно представлено только в одном направлении - вперед, от первого цикла (также можно двигаться в обратном направлении, используя встроенные функции, такие как <code>prev()</code>, <code>rose()</code> и <code>fell()</code>). Таким образом, простое PSL утверждение <code>assert a;</code> показывает, что a должно утверждаться в самом первом цикле, в то время как PSL утверждение <code>assert always a</code>, показывает, что a должно утверждаться в перовм цикле и в каждом следующем цикле, а это значит, что в каждом цикле. | ||
| + | <!-- | ||
By combining the temporal operators in various ways we can state properties | By combining the temporal operators in various ways we can state properties | ||
such as “every request receives an acknowledge”, “every acknowledged | such as “every request receives an acknowledge”, “every acknowledged | ||
| Строка 18: | Строка 22: | ||
“when we see a read request with tag equal to i, then on the next four data | “when we see a read request with tag equal to i, then on the next four data | ||
transfers we expect to see a tag of <code>i</code>”. | transfers we expect to see a tag of <code>i</code>”. | ||
| + | --> | ||
| + | Комбинированием временных операторов различными путями, мы можем установить свойства, такие как “каждый запрос получает подтверждение”, “каждому одтвержденному запросу предоставляется от четырех до семи циклов, в случаи, если запрос не приостановится первым”, | ||
The temporal layer is composed of the Foundation Language (FL) and the | The temporal layer is composed of the Foundation Language (FL) and the | ||
Версия 14:15, 25 октября 2013
- 1. Introduction (en)
- 2. Basic Temporal Properties (en)
- 3. Some Philosophy (en)
- 4. Weak vs. Strong Temporal Operators (en)
- 5. SERE Style (en)
Основные временные свойства While
В то время как Булевый слой состоит из Булевых выражений, которые выполняются или не выполняются в данном цикле, временной слой предоставляет путь для описания взаимоотношений между Булевыми выражениями по времени. PSL утверждение обычно представлено только в одном направлении - вперед, от первого цикла (также можно двигаться в обратном направлении, используя встроенные функции, такие как prev(), rose() и fell()). Таким образом, простое PSL утверждение assert a; показывает, что a должно утверждаться в самом первом цикле, в то время как PSL утверждение assert always a, показывает, что a должно утверждаться в перовм цикле и в каждом следующем цикле, а это значит, что в каждом цикле.
Комбинированием временных операторов различными путями, мы можем установить свойства, такие как “каждый запрос получает подтверждение”, “каждому одтвержденному запросу предоставляется от четырех до семи циклов, в случаи, если запрос не приостановится первым”,
The temporal layer is composed of the Foundation Language (FL) and the Optional Branching Extension (OBE). The FL is used to express properties of single traces, and can be used in either simulation or formal verification. The OBE is used to express properties referring to sets of traces, for example “there exists a trace such that ...”, and is used in formal verification. In this book we concentrate on the Foundation Language.
The Foundation Language itself is composed of two complementary styles – LTL style, named after the temporal logic LTL on which PSL is based, and SERE style, named after PSL’s Sequential Extended Regular Expressions, or SEREs. In this chapter we present the basic temporal operators of LTL style. We provide only a taste – enough to get the basic idea and to give some context to the philosophical issues that we discuss next.
Throughout this book, we make extensive use of examples. Each example property or assertion and its associated timing diagram (which we term a trace) are grouped together in a figure. Such a figure will contain one or more traces numbered with a parenthesized lower case Roman numeral, and one or more properties numbered by appending a lower case letter to the figure number. For instance, Figure 2.1 contains Trace 2.1(i) and Assertions 2.1a, 2.1b, and 2.1c.
