Project

General

Profile

Bug #1753

Analysis: Translation of imbricated structs to NuSMV

Added by Anonymous about 7 years ago. Updated over 6 years ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
09/23/2013
Due date:
% Done:

100%

Estimated time:

NestedStructs.af3_23 (7.47 KB) NestedStructs.af3_23 Andreas Bayha, 07/14/2014 11:33 AM

History

#1 Updated by Anonymous over 6 years ago

  • Assignee set to Anonymous

#2 Updated by Anonymous over 6 years ago

  • Subject changed from Translation of imbricated structs to NuSMV to Analysis: Translation of imbricated structs to NuSMV

#3 Updated by Anonymous over 6 years ago

  • Target version changed from Phoenix - BACKLOG to AF3 2.6 RC3 Quality fixed

#4 Updated by Anonymous over 6 years ago

  • % Done changed from 0 to 70

#5 Updated by Anonymous over 6 years ago

  • % Done changed from 70 to 80

#6 Updated by Anonymous over 6 years ago

  • Status changed from New to Resolved
  • Assignee changed from Anonymous to Andreas Bayha

#7 Updated by Anonymous over 6 years ago

  • % Done changed from 80 to 100

#8 Updated by Andreas Bayha over 6 years ago

Hi Vincent,

I tested a little bit and got an error message (Exception from console below).

On the project attached, I checked "Universally Globally: Output == 1".

java.lang.ClassCastException: org.fortiss.af3.expression.model.terms.impl.FunctionCallImpl cannot be cast to org.fortiss.af3.expression.model.terms.Var
at org.fortiss.af3.analyses.modelchecking.af3tonusmv.ModelCheckingLanguageComplianceChecker.checkVarComplexProperty(ModelCheckingLanguageComplianceChecker.java:305)
[...]

PS: I also tried an automaton specification for the component and got the same message.

#9 Updated by Anonymous over 6 years ago

  • Status changed from In Progress to Resolved
  • Assignee changed from Anonymous to Andreas Bayha
  • % Done changed from 90 to 100

#10 Updated by Andreas Bayha over 6 years ago

  • Status changed from Resolved to In Progress
  • Assignee changed from Andreas Bayha to Anonymous
  • % Done changed from 100 to 90

For the analysis "Universally Globally: Output == (Input.x).y" (on the Component in the above project), there is an exception thrown:

java.lang.ClassCastException: org.fortiss.af3.expression.model.terms.impl.FunctionCallImpl cannot be cast to org.fortiss.af3.expression.model.terms.Var
at org.fortiss.af3.analyses.base.AnalysesTypeChecker.typecheckMemberAccess(AnalysesTypeChecker.java:60)

#11 Updated by Anonymous over 6 years ago

  • Status changed from In Progress to Resolved
  • % Done changed from 90 to 100

#12 Updated by Anonymous over 6 years ago

  • Assignee changed from Anonymous to Andreas Bayha

#13 Updated by Andreas Bayha over 6 years ago

  • Assignee changed from Andreas Bayha to Anonymous

I did not found any counterexamples anymore :-)

I'm not sure whether Arrays would be expected to beeing able to be dealt with. If Arrays are not yet supposed to be supported, you can close this ticket :-)

#14 Updated by Anonymous over 6 years ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF