Project

General

Profile

Bug #1570

Check assume/guarantee Bug

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

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
08/03/2013
Due date:
% Done:

100%

Estimated time:

Description

- Check assume/guarantee under Assume/Guarantee Reasoning does not work under Component Architecture.
- Check selected Component under Assume/Guarantee Reasoning does not work for a component with a Code Specification.

Error log:


!ENTRY org.fortiss.af3.tools 1 0 2013-08-03 17:44:36.826
!MESSAGE Running z3 [z3, -smt2, assumption0b7-5564450619422312475.smt2] on file assumption0b7-5564450619422312475.smt2 in directory /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools.

!ENTRY org.fortiss.af3.tools 1 0 2013-08-03 17:44:36.868
!MESSAGE Run in 0,041s.

!ENTRY org.fortiss.af3.tools 4 0 2013-08-03 17:44:36.869
!MESSAGE Error on running z3 on file: /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools/assumption0b7-5564450619422312475.smt2 The file was not deleted and can be debugged!
java.util.concurrent.ExecutionException: java.lang.Exception: z3 exited with code 1 - 
    at java.util.concurrent.FutureTask$Sync.innerGet(FutureTask.java:232)
    at java.util.concurrent.FutureTask.get(FutureTask.java:91)
    at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:307)
    at org.fortiss.af3.analyses.smt.LazyLiftedAF3Result.get(SATAnalyzer.scala:72)
    at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:90)
    at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:85)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:174)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:103)
    at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
Caused by: java.lang.Exception: z3 exited with code 1 - 
    at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:136)
    at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:1)
    at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303)
    at java.util.concurrent.FutureTask.run(FutureTask.java:138)
    at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(ThreadPoolExecutor.java:895)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:918)
    at java.lang.Thread.run(Thread.java:680)

!ENTRY org.fortiss.af3.tools 4 0 2013-08-03 17:44:36.872
!MESSAGE Unexpected error!
!STACK 0
java.util.concurrent.ExecutionException: java.lang.Exception: z3 exited with code 1 - 
    at java.util.concurrent.FutureTask$Sync.innerGet(FutureTask.java:232)
    at java.util.concurrent.FutureTask.get(FutureTask.java:91)
    at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:307)
    at org.fortiss.af3.analyses.smt.LazyLiftedAF3Result.get(SATAnalyzer.scala:72)
    at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:90)
    at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:85)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:174)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:103)
    at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
Caused by: java.lang.Exception: z3 exited with code 1 - 
    at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:136)
    at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:1)
    at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303)
    at java.util.concurrent.FutureTask.run(FutureTask.java:138)
    at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(ThreadPoolExecutor.java:895)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:918)
    at java.lang.Thread.run(Thread.java:680)
java.lang.reflect.InvocationTargetException
    at org.eclipse.jface.operation.ModalContext.run(ModalContext.java:421)
    at org.eclipse.jface.dialogs.ProgressMonitorDialog.run(ProgressMonitorDialog.java:507)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar.doOpen(AnalysesProgressBar.java:99)
    at org.fortiss.af3.analyses.ui.ag.AssumeGuaranteeView.performAnalyzesAndDisplayResults(AssumeGuaranteeView.java:301)
    at org.fortiss.af3.analyses.ui.ag.AssumeGuaranteeView.access$0(AssumeGuaranteeView.java:280)
    at org.fortiss.af3.analyses.ui.ag.AssumeGuaranteeView$2.widgetSelected(AssumeGuaranteeView.java:191)
    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)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1480)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1465)
    at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1270)
    at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3974)
    at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3613)
    at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2701)
    at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2665)
    at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2499)
    at org.eclipse.ui.internal.Workbench$7.run(Workbench.java:679)
    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
    at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:668)
    at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
    at org.fortiss.af3.rcp.application.AF3Application.start(AF3Application.java:48)
    at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
    at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
    at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:344)
    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
    at java.lang.reflect.Method.invoke(Method.java:597)
    at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:622)
    at org.eclipse.equinox.launcher.Main.basicRun(Main.java:577)
    at org.eclipse.equinox.launcher.Main.run(Main.java:1410)
    at org.eclipse.equinox.launcher.Main.main(Main.java:1386)
Caused by: java.lang.RuntimeException: java.util.concurrent.ExecutionException: java.lang.Exception: z3 exited with code 1 - 
    at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:319)
    at org.fortiss.af3.analyses.smt.LazyLiftedAF3Result.get(SATAnalyzer.scala:72)
    at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:90)
    at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:85)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:174)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:103)
    at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
Caused by: java.util.concurrent.ExecutionException: java.lang.Exception: z3 exited with code 1 - 
    at java.util.concurrent.FutureTask$Sync.innerGet(FutureTask.java:232)
    at java.util.concurrent.FutureTask.get(FutureTask.java:91)
    at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:307)
    ... 6 more
Caused by: java.lang.Exception: z3 exited with code 1 - 
    at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:136)
    at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:1)
    at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303)
    at java.util.concurrent.FutureTask.run(FutureTask.java:138)
    at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(ThreadPoolExecutor.java:895)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:918)
    at java.lang.Thread.run(Thread.java:680)

For test see attached AF3 Project.

guarantee.af3_23 (31.6 KB) guarantee.af3_23 Anonymous, 08/03/2013 05:46 PM

History

#1 Updated by Anonymous about 7 years ago

assume guarantee under a component architecture should work (I've fixed it yesterday - please make an update)

#2 Updated by Anonymous about 7 years ago

I have now the current version, and I have tested it. The results are:

- If the Components under Component Architecture have no subcomponents, Check assume/guarantee works.
- If the Components under Component Architecture have subcomponents, Check assume/guarantee failed with the above mentioned error. So I can not check assume/guarantee under Component Architecture of the AF3 project that I have attached.

#3 Updated by Anonymous about 7 years ago

  • Status changed from New to Feedback
  • Assignee changed from Anonymous to Anonymous

I did a major fix in the AG analyses (compilation of AF3 expressions to z3). Please check whether this bug still exists.

#4 Updated by Anonymous about 7 years ago

Yes, it is still failed, but the error message is a little bit different:

!ENTRY org.fortiss.af3.tools 1 0 2013-08-04 18:47:16.376
!MESSAGE Running z3 [z3, -smt2, assumption0a6799807274903758262.smt2] on file assumption0a6799807274903758262.smt2 in directory /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools.

!ENTRY org.fortiss.af3.tools 1 0 2013-08-04 18:47:16.433
!MESSAGE Run in 0,056s.

!ENTRY org.fortiss.af3.tools 1 0 2013-08-04 18:47:16.434
!MESSAGE Parsing Z3 results!

!ENTRY org.fortiss.af3.tools 1 0 2013-08-04 18:47:16.435
!MESSAGE Running z3 [z3, -smt2, assumption0b77220863845500806582.smt2] on file assumption0b77220863845500806582.smt2 in directory /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools.

!ENTRY org.fortiss.af3.tools 1 0 2013-08-04 18:47:16.495
!MESSAGE Run in 0,059s.

!ENTRY org.fortiss.af3.tools 4 0 2013-08-04 18:47:16.495
!MESSAGE Error on running z3 on file: /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools/assumption0b77220863845500806582.smt2 The file was not deleted and can be debugged!
java.util.concurrent.ExecutionException: java.lang.Exception: z3 exited with code 1 - 

!ENTRY org.fortiss.af3.tools 4 0 2013-08-04 18:47:16.497
!MESSAGE Unexpected error!
    at java.util.concurrent.FutureTask$Sync.innerGet(FutureTask.java:232)
    at java.util.concurrent.FutureTask.get(FutureTask.java:91)
    at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:307)
    at org.fortiss.af3.analyses.smt.LazyLiftedAF3Result.get(SATAnalyzer.scala:72)
    at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:90)
    at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:85)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:174)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:103)
    at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
Caused by: java.lang.Exception: z3 exited with code 1 - 
    at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:136)
    at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:1)
    at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303)
    at java.util.concurrent.FutureTask.run(FutureTask.java:138)
    at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(ThreadPoolExecutor.java:895)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:918)
    at java.lang.Thread.run(Thread.java:680)
!STACK 0
java.util.concurrent.ExecutionException: java.lang.Exception: z3 exited with code 1 - 
    at java.util.concurrent.FutureTask$Sync.innerGet(FutureTask.java:232)
    at java.util.concurrent.FutureTask.get(FutureTask.java:91)
    at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:307)
    at org.fortiss.af3.analyses.smt.LazyLiftedAF3Result.get(SATAnalyzer.scala:72)
    at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:90)
    at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:85)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:174)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:103)
    at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
Caused by: java.lang.Exception: z3 exited with code 1 - 
    at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:136)
    at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:1)
    at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303)
    at java.util.concurrent.FutureTask.run(FutureTask.java:138)
    at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(ThreadPoolExecutor.java:895)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:918)
    at java.lang.Thread.run(Thread.java:680)
java.lang.reflect.InvocationTargetException
    at org.eclipse.jface.operation.ModalContext.run(ModalContext.java:421)
    at org.eclipse.jface.dialogs.ProgressMonitorDialog.run(ProgressMonitorDialog.java:507)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar.doOpen(AnalysesProgressBar.java:99)
    at org.fortiss.af3.analyses.ui.ag.AssumeGuaranteeView.performAnalyzesAndDisplayResults(AssumeGuaranteeView.java:301)
    at org.fortiss.af3.analyses.ui.ag.AssumeGuaranteeView.access$0(AssumeGuaranteeView.java:280)
    at org.fortiss.af3.analyses.ui.ag.AssumeGuaranteeView$1.widgetSelected(AssumeGuaranteeView.java:150)
    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)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1480)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1465)
    at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1270)
    at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3974)
    at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3613)
    at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2701)
    at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2665)
    at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2499)
    at org.eclipse.ui.internal.Workbench$7.run(Workbench.java:679)
    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
    at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:668)
    at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
    at org.fortiss.af3.rcp.application.AF3Application.start(AF3Application.java:48)
    at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
    at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
    at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:344)
    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
    at java.lang.reflect.Method.invoke(Method.java:597)
    at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:622)
    at org.eclipse.equinox.launcher.Main.basicRun(Main.java:577)
    at org.eclipse.equinox.launcher.Main.run(Main.java:1410)
    at org.eclipse.equinox.launcher.Main.main(Main.java:1386)
Caused by: java.lang.RuntimeException: java.util.concurrent.ExecutionException: java.lang.Exception: z3 exited with code 1 - 
    at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:319)
    at org.fortiss.af3.analyses.smt.LazyLiftedAF3Result.get(SATAnalyzer.scala:72)
    at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:90)
    at org.fortiss.af3.analyses.smt.ag.LazyAGResult.get(AssumeGuaranteeAnalyzerBase.scala:85)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:174)
    at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:103)
    at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
Caused by: java.util.concurrent.ExecutionException: java.lang.Exception: z3 exited with code 1 - 
    at java.util.concurrent.FutureTask$Sync.innerGet(FutureTask.java:232)
    at java.util.concurrent.FutureTask.get(FutureTask.java:91)
    at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:307)
    ... 6 more
Caused by: java.lang.Exception: z3 exited with code 1 - 
    at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:136)
    at org.fortiss.af3.tools.smtlib.run.Z3Runner$Z3Task.call(Z3Runner.java:1)
    at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303)
    at java.util.concurrent.FutureTask.run(FutureTask.java:138)
    at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(ThreadPoolExecutor.java:895)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:918)
    at java.lang.Thread.run(Thread.java:680)

#5 Updated by Anonymous about 7 years ago

  • Assignee changed from Anonymous to Anonymous

#6 Updated by Anonymous about 7 years ago

  • Status changed from Feedback to Resolved
  • Assignee changed from Anonymous to Anonymous
  • Target version set to Phoenix 2.4 RC3 (Review Phase)

it works now on my machine

#7 Updated by Anonymous about 7 years ago

  • Status changed from Resolved to Closed
  • Assignee changed from Anonymous to Anonymous
  • % Done changed from 0 to 100

It works also on my Laptop.

Also available in: Atom PDF