Property Specification Language: Difference between revisions

Revision as of 01:04, 18 November 2016

Revision as of 12:18, 23 November 2016

Line 178:

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

|-

| p untiluntil_ q

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

|-