Property Specification Language: Difference between revisions

Revision as of 16:13, 25 May 2017

Revision as of 16:18, 25 May 2017

Line 140:

|-

| never p

| property p does not holdshold on any time point

|-

| eventually! p

Line 176:

|-

| p until!_ q

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

|-

| p until_ q

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

|-

| p before! q