Property Specification Language: Difference between revisions

Revision as of 09:00, 26 May 2017

Revision as of 09:03, 26 May 2017

Line 136:

Here {{mono|p}} and {{mono|q}} are any PSL formulas.

{| class="wikitable"

| {{code|always p}}

| property p holds on every time point

|-

| {{code|never p}}

| property p does not hold on any time point

|-

| {{code|eventually! p}}

| there exists a future time point where p holds

|-

| {{code|next! p}}

| there exists a next time point, and p holds on this point

|-

| {{code|next p}}

| if there exists a next time point, then p holds on this point

|-

| {{code|next![n] p}}

| there exists an n-th time point, and p holds on this point

|-

| {{code|next[n] p}}

| if there exists an n-th time point, then p holds on this point

|-

| {{code|next_e![m..n] p}}

| there exists a time point, within m-th to n-th from the current where p holds.

|-

| {{code|next_e[m..n] p}}

| if there exists at least n-th time points, then p holds on one of the m-th to n-th points.

|-

| {{code|next_a![m..n] p}}

| there exists at least n more time points and p holds in all the time points between the m-th to the n-th, inclusive.

|-

| {{code|next_a[m..n] p}}

| p holds on all the next m-th through n-th time points, however many exist

|-

| {{code|p until! q}}

| there exists a time point where q holds, and p hold up until that time point

|-

| {{code|p until q}}

| p holds up until a time point where q hold, if such exists

|-

| {{code|p until!_ q}}

| there exists a time point where q holds, and p holds up until that time point and in that time point

|-

| {{code|p until_ q}}

| p holds up until a time point where q holds, and in that time point, if such exists

|-

| {{code|p before! q}}

| p holds strictly before the time point where q holds, and p eventually holds

|-

| {{code|p before q}}

| p holds strictly before the time point where q holds, if p never holds, then neither does q

|-

| {{code|p before!_ q}}

| p holds before or at the same time point where q holds, and p eventually holds

|-

| {{code|p before_ q}}

| p holds before or at the same time point where q holds, if p never holds, then neither does q

|-