Commit 5f4680e1 authored by Daniel Ratiu's avatar Daniel Ratiu
Browse files

making design by contract accessible from product

refs 814
parent b62bb88b
......@@ -122,6 +122,12 @@
id="org.fortiss.af3.rcp.application.semanticInspectorAction"
name="Semantic Inspector">
</command>
<command
categoryId="org.eclipse.ui.category.views"
defaultHandler="org.fortiss.af3.rcp.application.handler.ApplicationCommandHandler$OpenContractsSpecificationHandler"
id="org.fortiss.af3.rcp.application.contractsSpecificationAction"
name="Contracts Specification">
</command>
<command
categoryId="org.eclipse.ui.category.views"
defaultHandler="org.fortiss.af3.rcp.application.handler.ApplicationCommandHandler$OpenNondeterminismAnalysesCommandHandler"
......
......@@ -96,6 +96,9 @@ public class ApplicationActionBarAdvisor extends ActionBarAdvisor {
/** AF3-Specific Action to crate a new empty project. */
private static WorkbenchCommandAction newAF3ProjectAction;
/** Open the "Contracts Specification" view. */
private static WorkbenchCommandAction showContractsSpecificationAction;
/** Open the "Semantic Inspector" view. */
private static WorkbenchCommandAction showSemanticInspectorAction;
......@@ -388,6 +391,20 @@ public class ApplicationActionBarAdvisor extends ActionBarAdvisor {
aboutAction.setDescription("About AutoFOCUS3");
register(aboutAction);
// Open Contracts Specification.
{
actionText = "Contracts Specification";
showContractsSpecificationAction =
new WorkbenchCommandAction(
"org.fortiss.af3.rcp.application.contractsSpecificationAction", window);
showContractsSpecificationAction.setImageDescriptor(getPluginImageDescriptor(
"org.fortiss.af3.analyses.ui", "icons/contract.gif"));
showContractsSpecificationAction.setText(actionText);
showContractsSpecificationAction.setToolTipText(actionText);
showContractsSpecificationAction.setDescription(actionText);
register(showContractsSpecificationAction);
}
// Open Semantic Inspector (NuSMV).
{
actionText = "Semantic Inspector";
......@@ -487,6 +504,8 @@ public class ApplicationActionBarAdvisor extends ActionBarAdvisor {
toolBarManager.add(newAF3ProjectAction);
toolBarManager.add(saveAction);
toolBarManager.add(new Separator());
toolBarManager.add(showContractsSpecificationAction);
toolBarManager.add(new Separator());
toolBarManager.add(showSemanticInspectorAction);
toolBarManager.add(showNondeterminismAnalysesAction);
}
......
......@@ -455,6 +455,22 @@ public class ApplicationCommandHandler {
}
}
/** Handles the command action to open the "Contracts Specification View". */
public static final class OpenContractsSpecificationHandler extends AbstractHandler {
/** Opens the contracts specification view. */
@Override
public Object execute(ExecutionEvent event) {
try {
WorkbenchUtils.getActiveWorkbenchPage().showView(
"org.fortiss.af3.analyses.ui.contracts");
} catch(PartInitException e) {
e.printStackTrace();
}
return null;
}
}
/** Handles the command action to open the "Non-determinism Analyses View". */
public static final class OpenNondeterminismAnalysesCommandHandler extends AbstractHandler {
......
......@@ -167,7 +167,7 @@
</containedElements>
</specifications>
<specifications xsi:type="org-fortiss-af3-tlspec:TemporalLogicsSpecification">
<atoms analyzerID="ABSENCE_GLOBALLY" userFriendlyExplanation="Property 'P' is false Globally." checkResultStatus="-1">
<atoms atomID="ABSENCE_GLOBALLY" userFriendlyExplanation="Property 'P' is false Globally." checkResultStatus="-1">
<placeHolders>P</placeHolders>
<predicates>paced</predicates>
</atoms>
......@@ -308,13 +308,13 @@
</containedElements>
</specifications>
<specifications xsi:type="org-fortiss-af3-tlspec:TemporalLogicsSpecification">
<atoms analyzerID="RESPONSE_GLOBALLY" userFriendlyExplanation="'S' Responds to 'P' Globally." lastCheckDate="2012-02-27T13:38:51.233+0100">
<atoms atomID="RESPONSE_GLOBALLY" userFriendlyExplanation="'S' Responds to 'P' Globally." lastCheckDate="2012-02-27T13:38:51.233+0100">
<placeHolders>P</placeHolders>
<placeHolders>S</placeHolders>
<predicates>brady == true</predicates>
<predicates>paced == true</predicates>
</atoms>
<atoms analyzerID="EXISTENCE_AFTER" userFriendlyExplanation="'P' becomes true After 'Q'." lastCheckDate="2012-02-27T13:38:51.311+0100">
<atoms atomID="EXISTENCE_AFTER" userFriendlyExplanation="'P' becomes true After 'Q'." lastCheckDate="2012-02-27T13:38:51.311+0100">
<placeHolders>Q</placeHolders>
<placeHolders>P</placeHolders>
<predicates>brady == true</predicates>
......@@ -571,13 +571,13 @@
</dataStateVariables>
</specifications>
<specifications xsi:type="org-fortiss-af3-tlspec:TemporalLogicsSpecification">
<atoms analyzerID="EXISTENCE_AFTER" userFriendlyExplanation="'P' becomes true After 'Q'." lastCheckDate="2012-02-27T13:41:44.316+0100">
<atoms atomID="EXISTENCE_AFTER" userFriendlyExplanation="'P' becomes true After 'Q'." lastCheckDate="2012-02-27T13:41:44.316+0100">
<placeHolders>Q</placeHolders>
<placeHolders>P</placeHolders>
<predicates>timer >= 800</predicates>
<predicates>paced == true</predicates>
</atoms>
<atoms analyzerID="EXISTENCE_BEFORE" userFriendlyExplanation="'P' becomes true Before 'R'." lastCheckDate="2012-02-27T13:41:44.394+0100">
<atoms atomID="EXISTENCE_BEFORE" userFriendlyExplanation="'P' becomes true Before 'R'." lastCheckDate="2012-02-27T13:41:44.394+0100">
<placeHolders>P</placeHolders>
<placeHolders>R</placeHolders>
<predicates>paced != true</predicates>
......@@ -964,13 +964,13 @@
</specifications>
<specifications xsi:type="org-fortiss-af3-mira-usecase:ScopeSpecification" reference="3" id="804" name="Ref: 3"/>
<specifications xsi:type="org-fortiss-af3-tlspec:TemporalLogicsSpecification">
<atoms analyzerID="ABSENCE_BEFORE" userFriendlyExplanation="Property 'P' is false Before 'R'." lastCheckDate="2012-02-27T14:39:35.964+0100">
<atoms atomID="ABSENCE_BEFORE" userFriendlyExplanation="Property 'P' is false Before 'R'." lastCheckDate="2012-02-27T14:39:35.964+0100">
<placeHolders>P</placeHolders>
<placeHolders>R</placeHolders>
<predicates>paced == true</predicates>
<predicates>user_input != NoVal</predicates>
</atoms>
<atoms analyzerID="ABSENCE_GLOBALLY" userFriendlyExplanation="Property 'P' is false Globally." lastCheckDate="2012-02-27T14:39:36.073+0100">
<atoms atomID="ABSENCE_GLOBALLY" userFriendlyExplanation="Property 'P' is false Globally." lastCheckDate="2012-02-27T14:39:36.073+0100">
<placeHolders>P</placeHolders>
<predicates>paced == NoVal</predicates>
</atoms>
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment