Project

General

Profile

Bug #1498

Model checking of ports equality

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

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
07/18/2013
Due date:
% Done:

0%

Estimated time:

Description

I get a bug, when checking port properties of components (see screenshot and model attached)

The weakly component is modelled as a state machine with one state and the behavior "inputPort outputPort". The check is "inputPort outputPort".
You can see the counter example in the sreenshot.

SmallerModel.af3_23 (1.11 MB) SmallerModel.af3_23 Anonymous, 07/18/2013 11:50 AM
screenshot.PNG (243 KB) screenshot.PNG Anonymous, 07/18/2013 11:50 AM
screenshot.PNG (169 KB) screenshot.PNG Anonymous, 08/01/2013 01:10 PM
SMG_Model_v0.6.af3_23 (1.65 MB) SMG_Model_v0.6.af3_23 Anonymous, 08/01/2013 01:10 PM

History

#1 Updated by Anonymous over 7 years ago

  • Subject changed from model checking of ports to Model checking of ports equality
  • Status changed from New to Resolved
  • Assignee changed from Anonymous to Anonymous

#2 Updated by Anonymous about 7 years ago

Thank you for fixing that issue - now it works for the example above.

I tried a second expample and got an other error for ports equality, see model and screenshot attached.

Cheers, Denis

#3 Updated by Anonymous about 7 years ago

  • Target version changed from Phoenix 2.4 (Release August 2013) to Phoenix 2.4.1 (September 2013)

#4 Updated by Anonymous about 7 years ago

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

the property "sendConsumptionStatus == consumptionStatus" cannot be checked on "Consumption Persistency" component - the following exception occurs:

java.lang.RuntimeException: ImplementationFile for component Consumption Persistency could not be found.
at org.fortiss.af3.analyses.cprover.compiler.AF3ToCCompiler$.addPortInititalizationFunction(AF3ToCCompiler.scala:234)
at org.fortiss.af3.analyses.cprover.CProverBasedAnalyzer.compileComponent(CProverBasedAnalyzer.scala:150)
at org.fortiss.af3.analyses.cprover.CProverBasedAnalyzer.setUpCBMCInput(CProverBasedAnalyzer.scala:171)
at org.fortiss.af3.analyses.cprover.CProverBasedAnalyzer$CProverLiftedLazyResult.get(CProverBasedAnalyzer.scala:193)
at org.fortiss.af3.analyses.cprover.CProverBasedAnalyzer$CProverLiftedLazyResult.get(CProverBasedAnalyzer.scala:185)
at org.fortiss.af3.analyses.ui.cprover.CProverAnalysisView.performModelCheckingAndDisplayResults(CProverAnalysisView.java:304)
at org.fortiss.af3.analyses.ui.cprover.CProverAnalysisView.checkCondition(CProverAnalysisView.java:286)
at org.fortiss.af3.analyses.ui.cprover.CProverAnalysisView.access$2(CProverAnalysisView.java:276)
at org.fortiss.af3.analyses.ui.cprover.CProverAnalysisView$3.widgetSelected(CProverAnalysisView.java:268)
at org.eclipse.swt.widgets.TypedListener.handleEvent(TypedListener.java:240)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4128)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1457)

#5 Updated by Andreas Bayha about 7 years ago

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

The problem for CProver here is not the port equality itself, but the fact, that the analysed components's name contains whitespace.

Created new bug ticket #1678 for this issue.

#6 Updated by Anonymous about 7 years ago

  • Status changed from Resolved to Closed
  • Assignee deleted (Anonymous)

Also available in: Atom PDF