Project

General

Profile

Feature #3025

support for implication for expressions

Added by Anonymous about 3 years ago. Updated over 1 year ago.

Status:
Rejected
Priority:
Normal
Assignee:
-
Category:
-
Target version:
Start date:
08/04/2017
Due date:
% Done:

0%

Estimated time:

Description

add implication for expressions

History

#1 Updated by Anonymous about 3 years ago

  • Status changed from New to In Progress

#2 Updated by Anonymous about 3 years ago

  • Status changed from In Progress to Resolved
  • Assignee changed from Anonymous to Anonymous

Done as of 20945.

Use "->" for implication and "<->" for equivalence. Operators are translated to already present operators "==" for equivalence (just comparing two Booleans) and "!a | b" for "a -> b". This approach prevents integration problems with already existing code.

#3 Updated by Anonymous about 3 years ago

  • Status changed from Resolved to In Progress
  • Assignee changed from Anonymous to Anonymous

I do not want the translation to "!a | b". That decreases the readability of nusmv file.

Transformation needs to transform imply to imply.

#4 Updated by Anonymous about 3 years ago

I don't think it is a good idea to implement implications on a meta-model layer as it would require alterations in all compilers, transformers and everything that uses expressions.

#5 Updated by Anonymous about 3 years ago

  • Status changed from In Progress to Resolved
  • Assignee changed from Anonymous to Anonymous

added small code fragments in the NuSMV Text Generator to pretty-print Implications and double negation.

#6 Updated by Anonymous almost 3 years ago

  • Assignee changed from Anonymous to Anonymous

#7 Updated by Anonymous over 2 years ago

  • Assignee changed from Anonymous to Anonymous
  • Target version changed from AF3 2.12 Post-release to AF3 2.12 RC3 (Documented, code reviewed, tested)

@Sudeep: can you add a description about how this should be tested and assign it directly to Filip?
(also mention the classes to be reviewed if any)

#8 Updated by Anonymous over 2 years ago

  • Target version changed from AF3 2.12 RC3 (Documented, code reviewed, tested) to AF3 2.13 RC1 (Feature Freeze)

#9 Updated by Anonymous over 2 years ago

  • Status changed from Resolved to In Progress

#10 Updated by Anonymous over 2 years ago

  • Target version changed from AF3 2.13 RC1 (Feature Freeze) to AF3 2.14 RC1 (Feature Freeze)

#11 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.14 RC1 (Feature Freeze) to Backlog

#12 Updated by Anonymous over 1 year ago

  • Assignee changed from Anonymous to Johannes Eder

please reject.

#13 Updated by Johannes Eder over 1 year ago

  • Status changed from In Progress to Rejected
  • Assignee deleted (Johannes Eder)

Also available in: Atom PDF