Project

General

Profile

Bug #3610

Incorrect LTL Property Generation for Universality and Absence Before Patterns

Added by Anonymous over 1 year ago. Updated over 1 year ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
01/10/2019
Due date:
% Done:

0%

Estimated time:

Description

In Temporal Specifications the properties generated for following patterns do not match the mathematical definitions:

1. For Absence Before generated property is "<>P -> (!P U R)" whereas mathematical property is "<>R -> (!P U R)"
2. For Universality Before generated property is "<>P -> (P U R)" whereas mathematical property is "<>R -> (P U R)"

LTL patterns are described here: http://patterns.projects.cs.ksu.edu/documentation/patterns/ltl.shtml

History

#1 Updated by Anonymous over 1 year ago

  • Target version changed from AF3 2.14 Release to AF3 2.15 RC2 (Tested, Bug-free)

#2 Updated by Anonymous over 1 year ago

  • Description updated (diff)
  • Status changed from New to Resolved

#3 Updated by Anonymous over 1 year ago

  • Assignee changed from Anonymous to Anonymous

#4 Updated by Anonymous over 1 year ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF