Bug 514634 general Improvement
[Update] Overview Behavior Selection: adding some heuristic from Expert
Tab
Change-Id: I72b106e34418237e44c6279ff7fdc3b81017a08f
Signed-off-by: Arnault Lapitre <arnault.lapitre@cea.fr>
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/debug/DebugConfigurationPage.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/debug/DebugConfigurationPage.java
index 968c04e..a5a590c 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/debug/DebugConfigurationPage.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/debug/DebugConfigurationPage.java
@@ -179,7 +179,7 @@
Group group = widgetToolkit.createGroup(parent,
"Console Log", 2, 1, GridData.FILL_HORIZONTAL);
- widgetToolkit.createLabel(group, "&Verbose Level:", 1);
+ widgetToolkit.createLabel(group, "&Verbose Level :", 1);
fConsoleLevelCombo = widgetToolkit.createCombo(group,
SWT.DROP_DOWN | SWT.READ_ONLY, 1, CONSOLE_LEVEL_COMBO_ITEMS);
@@ -256,7 +256,7 @@
});
fGroupFirstSymbexOutputTrace = widgetToolkit.createGroup(
- comp, "&Trace:", 1, 2, GridData.FILL_BOTH);
+ comp, "&Trace ", 1, 2, GridData.FILL_BOTH);
fFirstSymbexOutputGraphizTraceStringField = new StringFieldEditor(
this, ATTR_FIRST_SYMBEX_OUTPUT_GRAPHVIZ_TRACE_SPEC,
"", fGroupFirstSymbexOutputTrace,
@@ -264,7 +264,7 @@
SWT.MULTI | SWT.WRAP | SWT.V_SCROLL);
fGroupFirstSymbexOutputFormat = widgetToolkit.createGroup(
- comp, "&Format:", 1, 2, GridData.FILL_BOTH);
+ comp, "&Format ", 1, 2, GridData.FILL_BOTH);
fFirstSymbexOutputGraphizFormatStringField = new StringFieldEditor(
this, ATTR_FIRST_SYMBEX_OUTPUT_GRAPHVIZ_FORMAT_SPEC,
"", fGroupFirstSymbexOutputFormat,
@@ -348,7 +348,7 @@
});
fGroupSecondSymbexOutputTrace = widgetToolkit.createGroup(
- comp, "&Trace:", 1, 2, GridData.FILL_BOTH);
+ comp, "&Trace ", 1, 2, GridData.FILL_BOTH);
fSecondSymbexOutputGraphizTraceStringField = new StringFieldEditor(
this, ATTR_SECOND_SYMBEX_OUTPUT_GRAPHVIZ_TRACE_SPEC,
"", fGroupSecondSymbexOutputTrace,
@@ -356,7 +356,7 @@
SWT.MULTI | SWT.WRAP | SWT.V_SCROLL);
fGroupSecondSymbexOutputFormat = widgetToolkit.createGroup(
- comp, "&Format:", 1, 2, GridData.FILL_BOTH);
+ comp, "&Format ", 1, 2, GridData.FILL_BOTH);
fSecondSymbexOutputGraphizFormatStringField = new StringFieldEditor(
this, ATTR_SECOND_SYMBEX_OUTPUT_GRAPHVIZ_FORMAT_SPEC,
"", fGroupSecondSymbexOutputFormat,
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/developer/DeveloperTuningConfigurationPage.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/developer/DeveloperTuningConfigurationPage.java
index 66c3460..6a9bc63 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/developer/DeveloperTuningConfigurationPage.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/developer/DeveloperTuningConfigurationPage.java
@@ -232,15 +232,15 @@
parent, 1, 5, GridData.FILL_HORIZONTAL);
fLogFileNameStringField = new StringFieldEditor(this,
- ATTR_DEVELOPER_TUNING_LOG_FILENAME, "&Log File:",comp,
+ ATTR_DEVELOPER_TUNING_LOG_FILENAME, "&Log File :",comp,
DEFAULT_DEVELOPER_TUNING_LOG_FILENAME);
fDebugTraceFileNameStringField = new StringFieldEditor(this,
- ATTR_DEVELOPER_TUNING_DEBUG_FILENAME, "&Debug File:", comp,
+ ATTR_DEVELOPER_TUNING_DEBUG_FILENAME, "&Debug File :", comp,
DEFAULT_DEVELOPER_TUNING_DEBUG_FILENAME);
- fDebugTraceLevelLabel = widgetToolkit.createLabel(comp, "&Debug Level:", 1);
+ fDebugTraceLevelLabel = widgetToolkit.createLabel(comp, "&Debug Level :", 1);
fDebugTraceLevelCombo = widgetToolkit.createCombo(comp,
SWT.DROP_DOWN | SWT.READ_ONLY, 1, TRACE_LEVEL_COMBO_ITEMS);
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/expert/ExpertBehaviorSelectionConfigurationProfile.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/expert/ExpertBehaviorSelectionConfigurationProfile.java
index b0bc16c..d720b0f 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/expert/ExpertBehaviorSelectionConfigurationProfile.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/expert/ExpertBehaviorSelectionConfigurationProfile.java
@@ -30,10 +30,10 @@
//
private IntegerFieldEditor fHoJBeginStep;
- private IntegerFieldEditor fHoJJumpHeight;
- private IntegerFieldEditor fHoJJumpLimit;
- private IntegerFieldEditor fHoJHitCount;
- private IntegerFieldEditor fHoJJumpCount;
+// private IntegerFieldEditor fHoJJumpHeight;
+// private IntegerFieldEditor fHoJJumpLimit;
+// private IntegerFieldEditor fHoJHitCount;
+// private IntegerFieldEditor fHoJJumpCount;
/**
@@ -69,7 +69,7 @@
fHoJBeginStep = new IntegerFieldEditor(fConfigurationPage,
ATTR_BEHAVIOR_SELECTION_HOJ_BEGIN_STEP,
- "&Begin Step:", comp1, 0);
+ "&Begin Step", comp1, 0);
fHoJBeginStep.setToolTipText("Number of \"cumulated\" steps "
+ "before begining the research of the behavior");
addField( fHoJBeginStep );
@@ -115,7 +115,7 @@
"&Search Locally scope instead Globally", comp, false) );
Group groupScheduler = widgetToolkit.createGroup(groupHoJProperty,
- "&Scheduler", 2, 2, GridData.FILL_HORIZONTAL);
+ "&Trace Sequence", 2, 2, GridData.FILL_HORIZONTAL);
Composite compScheduler = widgetToolkit.createComposite(
groupScheduler, 1, 1, GridData.FILL_HORIZONTAL);
@@ -144,7 +144,7 @@
ATTR_BEHAVIOR_SELECTION_HOJ_HIT_FOLDING,
"&Folding", compOption, true);
fieldEditor.setToolTipText(
- "Enabled checking many trace point in one context");
+ "Enabled verification of multiple trace properties per Symbex State");
addField( fieldEditor );
compOption = widgetToolkit.createComposite(
@@ -174,30 +174,38 @@
addField( fieldEditor );
- Group groupHoJHeuristic = widgetToolkit.createGroup(parent,
- "Section HEURISTIC", 1, 1, GridData.FILL_HORIZONTAL);
-
- Composite compHeuristic = widgetToolkit.createComposite(
- groupHoJHeuristic, 1, 1, GridData.FILL_HORIZONTAL);
- fHoJJumpHeight = new IntegerFieldEditor(fConfigurationPage,
- ATTR_BEHAVIOR_SELECTION_HOJ_JUMP_HEIGHT,
- "&Jump Height:", compHeuristic, 6);
- addField( fHoJJumpHeight );
-
- fHoJJumpLimit = new IntegerFieldEditor(fConfigurationPage,
- ATTR_BEHAVIOR_SELECTION_HOJ_JUMP_TRIALS_LIMIT,
- "&Jump Trials Limit:", compHeuristic, -1);
- addField( fHoJJumpLimit );
-
- fHoJHitCount = new IntegerFieldEditor(fConfigurationPage,
- ATTR_BEHAVIOR_SELECTION_HOJ_HIT_COUNT,
- "&Hit Count:", compHeuristic, 1);
- addField( fHoJHitCount );
-
- fHoJJumpCount = new IntegerFieldEditor(fConfigurationPage,
- ATTR_BEHAVIOR_SELECTION_HOJ_JUMP_COUNT,
- "&Jump Count:", compHeuristic, 1);
- addField( fHoJJumpCount );
+// Group groupHoJHeuristic = widgetToolkit.createGroup(parent,
+// "Section HEURISTIC ", 1, 1, GridData.FILL_HORIZONTAL);
+//
+// Composite compHeuristic = widgetToolkit.createComposite(
+// groupHoJHeuristic, 1, 1, GridData.FILL_HORIZONTAL);
+// fHoJJumpHeight = new IntegerFieldEditor(fConfigurationPage,
+// ATTR_BEHAVIOR_SELECTION_HOJ_JUMP_HEIGHT,
+// "&Exploration Height :", compHeuristic, 6);
+// fHoJJumpHeight.setToolTipText(
+// "Local exploration height before the next selection by HIT or JUMP");
+// addField( fHoJJumpHeight );
+//
+// fHoJJumpLimit = new IntegerFieldEditor(fConfigurationPage,
+// ATTR_BEHAVIOR_SELECTION_HOJ_JUMP_TRIALS_LIMIT,
+// "&Jump Trials Limit :", compHeuristic, -1);
+// fHoJJumpLimit.setToolTipText(
+// "Local exploration trials number for the Trace Sequence Coverage");
+// addField( fHoJJumpLimit );
+//
+// fHoJHitCount = new IntegerFieldEditor(fConfigurationPage,
+// ATTR_BEHAVIOR_SELECTION_HOJ_HIT_COUNT,
+// "&Hit Count :", compHeuristic, 1);
+// fHoJHitCount.setToolTipText(
+// "Number of paths to choose from HIT (i.e. new properties have been covered)");
+// addField( fHoJHitCount );
+//
+// fHoJJumpCount = new IntegerFieldEditor(fConfigurationPage,
+// ATTR_BEHAVIOR_SELECTION_HOJ_JUMP_COUNT,
+// "&Jump Count :", compHeuristic, 1);
+// fHoJJumpCount.setToolTipText(
+// "Number of paths to choose from JUMP (i.e. no new property covered)");
+// addField( fHoJJumpCount );
}
@@ -268,26 +276,26 @@
@Override
protected boolean isValidImpl(ILaunchConfiguration launchConfig) {
- if( ! fHoJBeginStep.isValid() ) {
- setErrorMessage("Begin Step is not a valid integer");
- return false;
- }
- if( ! fHoJJumpHeight.isValid() ) {
- setErrorMessage("Jump Height is not a valid integer");
- return false;
- }
- if( ! fHoJJumpLimit.isValid() ) {
- setErrorMessage("Jump Limit is not a valid integer");
- return false;
- }
- if( ! fHoJHitCount.isValid() ) {
- setErrorMessage("Hit Count is not a valid integer");
- return false;
- }
- if( ! fHoJJumpCount.isValid() ) {
- setErrorMessage("Jump Count is not a valid integer");
- return false;
- }
+// if( ! fHoJBeginStep.isValid() ) {
+// setErrorMessage("Begin Step is not a valid integer");
+// return false;
+// }
+// if( ! fHoJJumpHeight.isValid() ) {
+// setErrorMessage("Jump Height is not a valid integer");
+// return false;
+// }
+// if( ! fHoJJumpLimit.isValid() ) {
+// setErrorMessage("Jump Limit is not a valid integer");
+// return false;
+// }
+// if( ! fHoJHitCount.isValid() ) {
+// setErrorMessage("Hit Count is not a valid integer");
+// return false;
+// }
+// if( ! fHoJJumpCount.isValid() ) {
+// setErrorMessage("Jump Count is not a valid integer");
+// return false;
+// }
return true;
}
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/expert/ExpertTransitionCoverageConfigurationProfile.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/expert/ExpertTransitionCoverageConfigurationProfile.java
index 1f6e18d..0815ffe 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/expert/ExpertTransitionCoverageConfigurationProfile.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/expert/ExpertTransitionCoverageConfigurationProfile.java
@@ -179,7 +179,7 @@
// GridData.HORIZONTAL_ALIGN_BEGINNING);
fTCBeginStep = new IntegerFieldEditor(fConfigurationPage,
ATTR_TRANSITION_COVERAGE_BEGIN_STEP,
- "&Begin Step:", comp, 0);
+ "&Begin Step :", comp, 0);
fTCBeginStep.setToolTipText("Number of \"cumulated\" steps "
+ "before begining the verification cover");
fTCBeginStep.setEnabled(false);
@@ -225,7 +225,7 @@
Composite comp3 = widgetToolkit.createComposite(
groupTCProperty, 2, 1, GridData.FILL_HORIZONTAL);
- widgetToolkit.createLabel(comp3, "&Scope:", 1);
+ widgetToolkit.createLabel(comp3, "&Scope :", 1);
fTCScopeCombo = widgetToolkit.createCombo(comp3,
SWT.DROP_DOWN | SWT.READ_ONLY, 1, SCOPE_COMBO_ITEMS);
fTCScopeCombo.addSelectionListener(fListener);
@@ -242,14 +242,14 @@
comp = widgetToolkit.createComposite(
group, 2, 1, GridData.FILL_HORIZONTAL);
- widgetToolkit.createLabel(comp, "&Start:", 1);
+ widgetToolkit.createLabel(comp, "&Start :", 1);
fTCHeuristicStartCombo = widgetToolkit.createCombo(
comp, SWT.DROP_DOWN | SWT.READ_ONLY,
1, HEURISTIC_START_COMBO_ITEMS);
fTCHeuristicStartCombo.addSelectionListener(fListener);
fTCHeuristicTrials = new IntegerFieldEditor(fConfigurationPage,
- ATTR_TRANSITION_COVERAGE_HEURISTIC_TRIALS, "&Trials:", comp, -1);
+ ATTR_TRANSITION_COVERAGE_HEURISTIC_TRIALS, "&Trials :", comp, -1);
fTCHeuristicTrials.widthInChars = 10;
//fTCHeuristicTrials.setTextLimit(20);
addField(fTCHeuristicTrials);
@@ -262,13 +262,13 @@
group, 2, 1, GridData.FILL_HORIZONTAL);
fTCObjectiveRate = new IntegerFieldEditor(fConfigurationPage,
- ATTR_TRANSITION_COVERAGE_OBJECTIVE_RATE, "&Rate:", comp, 100);
+ ATTR_TRANSITION_COVERAGE_OBJECTIVE_RATE, "&Rate :", comp, 100);
//fTCObjectiveRate.widthInChars = 3;
fTCObjectiveRate.setTextLimit(3);
addField(fTCObjectiveRate);
fTCObjectiveRest = new IntegerFieldEditor(fConfigurationPage,
- ATTR_TRANSITION_COVERAGE_OBJECTIVE_REST, "&Rest:", comp, 0);
+ ATTR_TRANSITION_COVERAGE_OBJECTIVE_REST, "&Rest :", comp, 0);
//fTCObjectiveRest.widthInChars = 3;
fTCObjectiveRest.setTextLimit(3);
addField(fTCObjectiveRest);
@@ -281,11 +281,11 @@
group, 2, 1, GridData.FILL_HORIZONTAL);
fTCCoverageHeight = new IntegerFieldEditor(fConfigurationPage,
- ATTR_TRANSITION_COVERAGE_LOOKAHEAD_DEPTH, "&Depth:", comp, 7);
+ ATTR_TRANSITION_COVERAGE_LOOKAHEAD_DEPTH, "&Depth :", comp, 7);
addField(fTCCoverageHeight);
fTCCoverageHeightReachedLimit = new IntegerFieldEditor(fConfigurationPage,
- ATTR_TRANSITION_COVERAGE_LOOKAHEAD_WIDTH, "&Width:", comp, 42);
+ ATTR_TRANSITION_COVERAGE_LOOKAHEAD_WIDTH, "&Width :", comp, 42);
addField(fTCCoverageHeightReachedLimit);
@@ -312,7 +312,7 @@
fTCHitStronglyCount = new IntegerFieldEditor(fConfigurationPage,
ATTR_TRANSITION_COVERAGE_HIT_STRONGLY_COUNT,
- "&Hit Count:", compGroup, 1);
+ "&Hit Count :", compGroup, 1);
addField(fTCHitStronglyCount);
@@ -333,7 +333,7 @@
fTCHitWeaklyCount = new IntegerFieldEditor(fConfigurationPage,
ATTR_TRANSITION_COVERAGE_HIT_WEAKLY_COUNT,
- "&Hit Count:", compGroup, 1);
+ "&Hit Count :", compGroup, 1);
addField(fTCHitWeaklyCount);
@@ -354,7 +354,7 @@
fTCHitOtherCount = new IntegerFieldEditor(fConfigurationPage,
ATTR_TRANSITION_COVERAGE_HIT_OTHER_COUNT,
- "&Hit Count:", compGroup, 1);
+ "&Hit Count :", compGroup, 1);
addField(fTCHitOtherCount);
@@ -369,7 +369,7 @@
comp = widgetToolkit.createComposite(
group, 1, 1, GridData.FILL_HORIZONTAL);
- widgetToolkit.createLabel(comp, "&Heuristic:", 1);
+ widgetToolkit.createLabel(comp, "&Heuristic :", 1);
fTCDirectiveTraceHeuristicCombo = widgetToolkit.createCombo(
comp, SWT.DROP_DOWN | SWT.READ_ONLY, 1,
DIRECTIVE_TRACE_HEURISTIC_COMBO_ITEMS);
@@ -377,12 +377,12 @@
fTCDirectiveTraceCountLimit = new IntegerFieldEditor(fConfigurationPage,
ATTR_TRANSITION_COVERAGE_DIRECTIVE_TRACE_COUNT_LIMIT,
- "&Count:", comp, 8);
+ "&Count :", comp, 8);
addField(fTCDirectiveTraceCountLimit);
fTCDirectiveTraceSizeLimit = new IntegerFieldEditor(fConfigurationPage,
ATTR_TRANSITION_COVERAGE_DIRECTIVE_TRACE_SIZE_LIMIT,
- "&Size:", comp, 8);
+ "&Size :", comp, 8);
addField(fTCDirectiveTraceSizeLimit);
}
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/nonregression/NonRegressionConfigurationPage.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/nonregression/NonRegressionConfigurationPage.java
index 13f4e1a..bec2320 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/nonregression/NonRegressionConfigurationPage.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/nonregression/NonRegressionConfigurationPage.java
@@ -232,7 +232,7 @@
new ElementTreeSelectionDialog(parent.getShell(),
new WorkbenchLabelProvider(),
new WorkbenchContentProvider());
- dialog.setTitle("Select a &Diversity Specification:");
+ dialog.setTitle("Select a &Diversity Specification");
dialog.setMessage("Select a resource to redirect output to:");
dialog.setInput(ResourcesPlugin.getWorkspace().getRoot());
dialog.setComparator(
@@ -254,7 +254,7 @@
// org.eclipse.ui.dialogs.ResourceSelectionDialog dialog =
// new ResourceSelectionDialog(getShell(),
// ResourcesPlugin.getWorkspace().getRoot(),
-// "Select a &Diversity Specification:");
+// "Select a &Diversity Specification");
//
// if(dialog.open() == Window.OK) {
// Object[] results = dialog.getResult();
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewBehaviorSelectionConfigurationProfile.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewBehaviorSelectionConfigurationProfile.java
index 01e3535..1fbd320 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewBehaviorSelectionConfigurationProfile.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewBehaviorSelectionConfigurationProfile.java
@@ -17,12 +17,30 @@
import org.eclipse.efm.execution.configuration.common.ui.api.AbstractConfigurationPage;
import org.eclipse.efm.execution.configuration.common.ui.api.AbstractConfigurationProfile;
import org.eclipse.efm.execution.configuration.common.ui.api.IWidgetToolkit;
+import org.eclipse.efm.execution.configuration.common.ui.editors.IntegerFieldEditor;
import org.eclipse.efm.execution.configuration.common.ui.editors.StringFieldEditor;
import org.eclipse.swt.SWT;
+import org.eclipse.swt.layout.GridData;
import org.eclipse.swt.widgets.Composite;
+import org.eclipse.swt.widgets.Group;
public class OverviewBehaviorSelectionConfigurationProfile extends AbstractConfigurationProfile {
+ private Group groupSelectionHeuristic;
+
+ private Group groupExplorationHeuristic;
+
+ private IntegerFieldEditor fHoJLocalHeight;
+ private IntegerFieldEditor fHoJTrialLimit;
+
+ private Group groupHitOrJumpHeuristic;
+
+ private IntegerFieldEditor fHoJHitCount;
+ private IntegerFieldEditor fHoJJumpCount;
+
+
+ private Group groupTraceSequence;
+
private StringFieldEditor fBehaviorSpecificationStringField;
@@ -50,16 +68,90 @@
protected void createContent(Composite parent, IWidgetToolkit widgetToolkit) {
parent.setToolTipText(BEHAVIOR_DESCRIPTION);
+ Composite container = widgetToolkit.createComposite(
+ parent, 1, 1, GridData.FILL_HORIZONTAL);
+
+ // Trace Sequence
+ groupTraceSequence = widgetToolkit.createGroup(
+ container, "&Trace Sequence ", 1, 1, GridData.FILL_HORIZONTAL);
+
+ Composite comp = widgetToolkit.createComposite(
+ groupTraceSequence, 1, 1, GridData.FILL_HORIZONTAL);
+
fBehaviorSpecificationStringField = new StringFieldEditor(fConfigurationPage,
ATTR_BEHAVIOR_ANALYSIS_ELEMENT_NAME_LIST, "",
- parent, BEHAVIOR_DESCRIPTION, SWT.MULTI | SWT.WRAP | SWT.V_SCROLL);
+ comp, BEHAVIOR_DESCRIPTION, SWT.MULTI | SWT.WRAP | SWT.V_SCROLL);
fBehaviorSpecificationStringField.setToolTipText(BEHAVIOR_DESCRIPTION);
addField(fBehaviorSpecificationStringField);
+
+
+ // Selection Heuristic
+ groupSelectionHeuristic = widgetToolkit.createGroup(container,
+ "&Exploration && Selection Heuristic ", 2, 1, GridData.FILL_HORIZONTAL);
+
+// comp = widgetToolkit.createComposite(
+// groupSelectionHeuristic, 1, 1, GridData.FILL_HORIZONTAL);
+
+ // Exploration Heuristic
+ groupExplorationHeuristic = widgetToolkit.createGroup(groupSelectionHeuristic,
+ "&Local Exploration Limit ", 1, 1, GridData.FILL_HORIZONTAL);
+
+ comp = widgetToolkit.createComposite(
+ groupExplorationHeuristic, 1, 1, GridData.FILL_HORIZONTAL);
+
+ // Local exploration height before the next selection by HIT or JUMP
+ fHoJLocalHeight = new IntegerFieldEditor(fConfigurationPage,
+ ATTR_BEHAVIOR_SELECTION_HOJ_JUMP_HEIGHT,
+ "&Height :", comp, 6);
+ fHoJLocalHeight.setToolTipText(
+ "Local exploration height before the next selection by HIT or JUMP");
+ addField( fHoJLocalHeight );
+
+ // Local exploration trials number
+ fHoJTrialLimit = new IntegerFieldEditor(fConfigurationPage,
+ ATTR_BEHAVIOR_SELECTION_HOJ_JUMP_TRIALS_LIMIT,
+ "&Trials :", comp, -1);
+ fHoJTrialLimit.setToolTipText(
+ "Local exploration trials number for the Trace Sequence Coverage");
+ addField( fHoJTrialLimit );
+
+ // HIT or JUMP Heuristic
+ groupHitOrJumpHeuristic = widgetToolkit.createGroup(groupSelectionHeuristic,
+ "&Hit or Jump Selection Count ", 1, 1, GridData.FILL_HORIZONTAL);
+
+ comp = widgetToolkit.createComposite(
+ groupHitOrJumpHeuristic, 1, 1, GridData.FILL_HORIZONTAL);
+
+
+ // Number of paths to choose from HIT
+ fHoJHitCount = new IntegerFieldEditor(fConfigurationPage,
+ ATTR_BEHAVIOR_SELECTION_HOJ_HIT_COUNT,
+ "&Hit :", comp, 1);
+ fHoJHitCount.setToolTipText(
+ "Number of paths to choose when HIT (i.e. new properties have been covered)");
+ addField( fHoJHitCount );
+
+ // Number of paths to choose from JUMP
+ fHoJJumpCount = new IntegerFieldEditor(fConfigurationPage,
+ ATTR_BEHAVIOR_SELECTION_HOJ_JUMP_COUNT,
+ "&Jump :", comp, 1);
+ fHoJJumpCount.setToolTipText(
+ "Number of paths to choose when JUMP (i.e. no new property covered)");
+ addField( fHoJJumpCount );
}
@Override
protected void setDefaultsImpl(ILaunchConfigurationWorkingCopy configuration) {
+ configuration.setAttribute(ATTR_BEHAVIOR_SELECTION_HOJ_JUMP_HEIGHT, 6);
+
+ configuration.setAttribute(
+ ATTR_BEHAVIOR_SELECTION_HOJ_JUMP_TRIALS_LIMIT, -1);
+
+ configuration.setAttribute(ATTR_BEHAVIOR_SELECTION_HOJ_HIT_COUNT, 1);
+
+ configuration.setAttribute(ATTR_BEHAVIOR_SELECTION_HOJ_JUMP_COUNT, 1);
+
configuration.setAttribute(
ATTR_BEHAVIOR_ANALYSIS_ELEMENT_NAME_LIST,
BEHAVIOR_INITIAL_SAMPLE);
@@ -77,6 +169,25 @@
@Override
protected boolean isValidImpl(ILaunchConfiguration launchConfig) {
+ // Exploration Heuristic Validation
+ if( ! fHoJLocalHeight.isValid() ) {
+ setErrorMessage("Jump Height is not a valid integer");
+ return false;
+ }
+ if( ! fHoJTrialLimit.isValid() ) {
+ setErrorMessage("Jump Limit is not a valid integer");
+ return false;
+ }
+ if( ! fHoJHitCount.isValid() ) {
+ setErrorMessage("Hit Count is not a valid integer");
+ return false;
+ }
+ if( ! fHoJJumpCount.isValid() ) {
+ setErrorMessage("Jump Count is not a valid integer");
+ return false;
+ }
+
+ // Trace Sequence Validation
String[] tabString = fBehaviorSpecificationStringField
.getStringValue().split(";\n");
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewConfigurationPage.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewConfigurationPage.java
index cb698a4..3870799 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewConfigurationPage.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewConfigurationPage.java
@@ -150,7 +150,7 @@
parent.getShell(),
new WorkbenchLabelProvider(),
new WorkbenchContentProvider() );
- dialog.setTitle("Select a Diversity Specification:");
+ dialog.setTitle("Select a Diversity Specification");
dialog.setMessage("Select a resource to redirect output to:");
dialog.setInput(ResourcesPlugin.getWorkspace().getRoot());
dialog.setComparator(
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewTestOfflineConfigurationProfile.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewTestOfflineConfigurationProfile.java
index 3d40a5a..6bd4e0e 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewTestOfflineConfigurationProfile.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewTestOfflineConfigurationProfile.java
@@ -139,7 +139,7 @@
fCompositeParent.getShell(),
new WorkbenchLabelProvider(),
new WorkbenchContentProvider() );
- dialog.setTitle("Select a Resource:");
+ dialog.setTitle("Select a Resource");
dialog.setMessage("Select a resource to redirect output to:");
dialog.setInput(ResourcesPlugin.getWorkspace().getRoot());
dialog.setComparator(
@@ -185,7 +185,7 @@
fCompositeParent.getShell(),
new WorkbenchLabelProvider(),
new WorkbenchContentProvider());
- dialog.setTitle("Select a Resource:");
+ dialog.setTitle("Select a Resource");
dialog.setMessage(
"Select a resource to redirect output to:");
dialog.setInput(
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewWorkspaceDataSection.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewWorkspaceDataSection.java
index 041459d..9eccee4 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewWorkspaceDataSection.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/overview/OverviewWorkspaceDataSection.java
@@ -64,7 +64,7 @@
fWorkspaceRootLocationStringField =
new StringFieldEditor(fConfigurationPage,
- ATTR_WORKSPACE_ROOT_LOCATION, "Location", parent, root);
+ ATTR_WORKSPACE_ROOT_LOCATION, "Location :", parent, root);
fWorkspaceRootLocationStringField.setEnabled(false);
fWorkspaceRootLocationStringField.setToolTipText(toolTipText2);
fWorkspaceRootLocationStringField.setEmptyStringAllowed(false);
@@ -72,7 +72,7 @@
fWorkspaceOutputLocationStringField =
new StringFieldEditor(fConfigurationPage,
- ATTR_WORKSPACE_OUTPUT_FOLDER_NAME, "Output", parent,
+ ATTR_WORKSPACE_OUTPUT_FOLDER_NAME, "Output :", parent,
DEFAULT_WORKSPACE_OUTPUT_FOLDER_NAME);
fWorkspaceOutputLocationStringField.setToolTipText(toolTipText2);
addField(fWorkspaceOutputLocationStringField);
@@ -81,7 +81,7 @@
if( getConfigurationPage().isEnabledSymbexDeveloperMode() ) {
StringFieldEditor folderNameStringFieldEditor =
new StringFieldEditor(fConfigurationPage,
- ATTR_WORKSPACE_LOG_FOLDER_NAME, "Log",
+ ATTR_WORKSPACE_LOG_FOLDER_NAME, "Log :",
parent, DEFAULT_WORKSPACE_LOG_FOLDER_NAME);
folderNameStringFieldEditor.setToolTipText(toolTipText3);
addField(folderNameStringFieldEditor);
@@ -89,7 +89,7 @@
folderNameStringFieldEditor =
new StringFieldEditor(fConfigurationPage,
- ATTR_WORKSPACE_DEBUG_FOLDER_NAME, "Debug",
+ ATTR_WORKSPACE_DEBUG_FOLDER_NAME, "Debug :",
parent, DEFAULT_WORKSPACE_DEBUG_FOLDER_NAME);
folderNameStringFieldEditor.setToolTipText(toolTipText3);
addField(folderNameStringFieldEditor);
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/supervisor/SupervisorEvaluationLimitsSection.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/supervisor/SupervisorEvaluationLimitsSection.java
index 97cfa76..89d6526 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/supervisor/SupervisorEvaluationLimitsSection.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/supervisor/SupervisorEvaluationLimitsSection.java
@@ -51,21 +51,21 @@
{
IntegerFieldEditor integerField = new IntegerFieldEditor(fConfigurationPage,
ATTR_SPECIFICATION_STOP_CRITERIA_STEPS,
- "&Symbex Step Count:", parent, 1000);
+ "&Symbex Step Count :", parent, 1000);
integerField.setToolTipText("Maximal symbex step (possibly many evaluations by step)"
+ " (-1 <=> no-limit) during the dynamic process");
addField( integerField );
integerField = new IntegerFieldEditor(fConfigurationPage,
ATTR_SPECIFICATION_STOP_CRITERIA_EVALS,
- "&Symbex Eval Count:", parent, 1000);
+ "&Symbex Eval Count :", parent, 1000);
integerField.setToolTipText("Maximal symbex evaluation count"
+ " (-1 <=> no-limit) during the dynamic process");
addField( integerField );
integerField = new IntegerFieldEditor(fConfigurationPage,
ATTR_SPECIFICATION_STOP_CRITERIA_TIMEOUT,
- "&Timeout (seconds):", parent, -1);
+ "&Timeout (seconds) :", parent, -1);
integerField.setToolTipText("Maximal duration "
+ "(-1 <=> no-limit) of the symbex dynamic process");
addField( integerField );
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/supervisor/SupervisorGraphSizeLimitsSection.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/supervisor/SupervisorGraphSizeLimitsSection.java
index e9cb4fa..d504127 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/supervisor/SupervisorGraphSizeLimitsSection.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/supervisor/SupervisorGraphSizeLimitsSection.java
@@ -49,19 +49,19 @@
protected void createContent(Composite parent, IWidgetToolkit widgetToolkit)
{
IntegerFieldEditor integerField = new IntegerFieldEditor(fConfigurationPage,
- ATTR_SPECIFICATION_STOP_CRITERIA_NODE, "&Nodes:", parent, -1);
+ ATTR_SPECIFICATION_STOP_CRITERIA_NODE, "&Nodes :", parent, -1);
integerField.setToolTipText("Maximal number of nodes "
+ "(-1 <=> no-limit) of the symbolic execution tree");
addField( integerField );
integerField = new IntegerFieldEditor(fConfigurationPage,
- ATTR_SPECIFICATION_STOP_CRITERIA_WIDTH, "W&idth:", parent, -1);
+ ATTR_SPECIFICATION_STOP_CRITERIA_WIDTH, "W&idth :", parent, -1);
integerField.setToolTipText(
"Maximal width (-1 <=> no-limit) of the symbolic execution tree");
addField( integerField );
integerField = new IntegerFieldEditor(fConfigurationPage,
- ATTR_SPECIFICATION_STOP_CRITERIA_HEIGHT, "&Height:", parent, 100);
+ ATTR_SPECIFICATION_STOP_CRITERIA_HEIGHT, "&Height :", parent, 100);
integerField.setToolTipText(
"Maximal height (-1 <=> no-limit) of the symbolic execution tree");
addField( integerField );
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/testgen/TestGenerationBasicTraceConfigurationProfile.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/testgen/TestGenerationBasicTraceConfigurationProfile.java
index 1699d0d..d3a90de 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/testgen/TestGenerationBasicTraceConfigurationProfile.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/testgen/TestGenerationBasicTraceConfigurationProfile.java
@@ -114,7 +114,7 @@
StringFieldEditor resourceNameStringField =
new StringFieldEditor(fConfigurationPage,
- ATTR_BASIC_TRACE_FOLDER_NAME, "&Folder:",
+ ATTR_BASIC_TRACE_FOLDER_NAME, "&Folder :",
comp, DEFAULT_BASIC_TRACE_FOLDER_NAME);
resourceNameStringField.setToolTipText(
"Folder name w.r.t. <workspace-root>/<output>");
@@ -124,7 +124,7 @@
groupBasicConfiguration, 1, 1, GridData.FILL_HORIZONTAL);
resourceNameStringField = new StringFieldEditor(fConfigurationPage,
- ATTR_BASIC_TRACE_FILE_NAME, "&File:",
+ ATTR_BASIC_TRACE_FILE_NAME, "&File :",
comp, DEFAULT_BASIC_TRACE_FILE_NAME);
resourceNameStringField.setToolTipText("File name");
addField(resourceNameStringField);
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/testgen/TestGenerationConfigurationPage.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/testgen/TestGenerationConfigurationPage.java
index c10cbfe..71e78c1 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/testgen/TestGenerationConfigurationPage.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/testgen/TestGenerationConfigurationPage.java
@@ -109,14 +109,14 @@
fTraceExtensionEvaluationStepsLimitIntegerField =
new IntegerFieldEditor(this,
ATTR_TRACE_EXTENSION_EVALUATION_STEPS,
- "&Evaluation Steps:", comp, -1);
+ "&Evaluation Steps :", comp, -1);
fTraceExtensionEvaluationStepsLimitIntegerField.setToolTipText(
"Maximal evaluation steps (-1 <=> no-limit) " +
"during the extension of symbolic execution");
Group group = widgetToolkit.createGroup(
- groupTraceExtension, "Trace Ending with:",
+ groupTraceExtension, "Trace Ending with ",
1, 1, GridData.FILL_HORIZONTAL);
fTraceExtensionObjectiveStringField = new StringFieldEditor(
diff --git a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/testgen/TestGenerationTTCNConfigurationProfile.java b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/testgen/TestGenerationTTCNConfigurationProfile.java
index f9e95df..d3d9efd 100644
--- a/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/testgen/TestGenerationTTCNConfigurationProfile.java
+++ b/execution/org.eclipse.efm.execution.configuration.common.ui/src/org/eclipse/efm/execution/configuration/common/ui/page/testgen/TestGenerationTTCNConfigurationProfile.java
@@ -128,7 +128,7 @@
StringFieldEditor folderNameStringField =
new StringFieldEditor(fConfigurationPage,
- ATTR_TTCN_FOLDER_NAME, "&Folder:", comp,
+ ATTR_TTCN_FOLDER_NAME, "&Folder :", comp,
DEFAULT_TTCN_FOLDER_NAME);
folderNameStringField.setToolTipText(
"Folder name w.r.t. <workspace-root>/<output>");
@@ -156,7 +156,7 @@
addField( new StringFieldEditor(fConfigurationPage,
ATTR_TTCN_CONTROL_MODULE_NAME,
- "&Name:", comp,
+ "&Name :", comp,
DEFAULT_TTCN_CONTROL_MODULE_NAME) );
}
@@ -169,7 +169,7 @@
addField( new StringFieldEditor(fConfigurationPage,
ATTR_TTCN_DECLARATIONS_MODULE_NAME,
- "&Name:", comp,
+ "&Name :", comp,
DEFAULT_TTCN_DECLARATIONS_MODULE_NAME) );
}
@@ -182,7 +182,7 @@
addField( new StringFieldEditor(fConfigurationPage,
ATTR_TTCN_TEMPLATES_MODULE_NAME,
- "&Name:", comp,
+ "&Name :", comp,
DEFAULT_TTCN_TEMPLATE_MODULE_NAME) );
}
@@ -197,7 +197,7 @@
addField( new StringFieldEditor(fConfigurationPage,
ATTR_TTCN_TESTCASES_MODULE_NAME,
- "&Name:", comp,
+ "&Name :", comp,
DEFAULT_TTCN_TESTCASES_MODULE_NAME) );
Group groupAdapters = widgetToolkit.createGroup(group,
@@ -218,7 +218,7 @@
StringFieldEditor wrapperStringField = new StringFieldEditor(
fConfigurationPage, ATTR_TTCN_TESTCASES_STARTING_WRAPPER,
- "&Starting:", comp, DEFAULT_TTCN_TESTCASES_STARTING_WRAPPER,
+ "&Starting :", comp, DEFAULT_TTCN_TESTCASES_STARTING_WRAPPER,
SWT.MULTI | SWT.WRAP | SWT.V_SCROLL);
wrapperStringField.setToolTipText(
HELPER_MODULE_TESTCASE_STARTING_ENDING_PATTERN_PARAMETERS );
@@ -226,7 +226,7 @@
wrapperStringField = new StringFieldEditor(
fConfigurationPage, ATTR_TTCN_TESTCASES_ENDING_WRAPPER,
- "&Ending:", comp, DEFAULT_TTCN_TESTCASES_ENDING_WRAPPER,
+ "&Ending :", comp, DEFAULT_TTCN_TESTCASES_ENDING_WRAPPER,
SWT.MULTI | SWT.WRAP | SWT.V_SCROLL);
wrapperStringField.setToolTipText(
HELPER_MODULE_TESTCASE_STARTING_ENDING_PATTERN_PARAMETERS );
@@ -245,7 +245,7 @@
wrapperStringField = new StringFieldEditor(
fConfigurationPage, ATTR_TTCN_TESTCASES_SENDING_WRAPPER,
- "&Sending:", comp, DEFAULT_TTCN_TESTCASES_SENDING_WRAPPER,
+ "&Sending :", comp, DEFAULT_TTCN_TESTCASES_SENDING_WRAPPER,
SWT.MULTI | SWT.WRAP | SWT.V_SCROLL);
wrapperStringField.setToolTipText(
HELPER_MODULE_TESTCASE_COMMUNICATION_PATTERN_PARAMETERS );
@@ -253,7 +253,7 @@
wrapperStringField = new StringFieldEditor(
fConfigurationPage, ATTR_TTCN_TESTCASES_RECEIVING_WRAPPER,
- "&Receiving:", comp, DEFAULT_TTCN_TESTCASES_RECEIVING_WRAPPER,
+ "&Receiving :", comp, DEFAULT_TTCN_TESTCASES_RECEIVING_WRAPPER,
SWT.MULTI | SWT.WRAP | SWT.V_SCROLL);
wrapperStringField.setToolTipText(
HELPER_MODULE_TESTCASE_COMMUNICATION_PATTERN_PARAMETERS );
@@ -271,7 +271,7 @@
group, 2, 1, GridData.FILL_HORIZONTAL);
addField( new StringFieldEditor(fConfigurationPage,
- ATTR_TTCN_ADAPTATION_MODULE_NAME, "&Name:",
+ ATTR_TTCN_ADAPTATION_MODULE_NAME, "&Name :",
comp, DEFAULT_TTCN_ADAPTATION_MODULE_NAME) );
diff --git a/execution/org.eclipse.efm.execution.core/src/org/eclipse/efm/execution/core/workflow/common/DeveloperTuningOptionCustomImpl.java b/execution/org.eclipse.efm.execution.core/src/org/eclipse/efm/execution/core/workflow/common/DeveloperTuningOptionCustomImpl.java
index c934e76..fa3f079 100644
--- a/execution/org.eclipse.efm.execution.core/src/org/eclipse/efm/execution/core/workflow/common/DeveloperTuningOptionCustomImpl.java
+++ b/execution/org.eclipse.efm.execution.core/src/org/eclipse/efm/execution/core/workflow/common/DeveloperTuningOptionCustomImpl.java
@@ -711,6 +711,7 @@
String strOutputFilename = getOutputFilename();
String strSpecificationFilename = getSpecificationFilename();
String strExecutableFilename = getExecutableFilename();
+ String strInitializationFilename = getExecutableFilename();
String strScenariiFilename = getSymbexGraphFilename();
if( (strOutputFilename != null)
@@ -735,6 +736,11 @@
.append( strExecutableFilename ).appendEol( "'" );
}
+ if( strExecutableFilename != null ) {
+ writer.appendTab2( "initialization = '" )
+ .append( strInitializationFilename ).appendEol( "'" );
+ }
+
if( strScenariiFilename != null ) {
writer.appendTab2( "scenarii = '" )
.append( strScenariiFilename ).appendEol( "'" );
diff --git a/execution/org.eclipse.efm.execution.core/src/org/eclipse/efm/execution/core/workflow/coverage/BehaviorCoverageWorkerCustomImpl.java b/execution/org.eclipse.efm.execution.core/src/org/eclipse/efm/execution/core/workflow/coverage/BehaviorCoverageWorkerCustomImpl.java
index c87440f..4babc35 100644
--- a/execution/org.eclipse.efm.execution.core/src/org/eclipse/efm/execution/core/workflow/coverage/BehaviorCoverageWorkerCustomImpl.java
+++ b/execution/org.eclipse.efm.execution.core/src/org/eclipse/efm/execution/core/workflow/coverage/BehaviorCoverageWorkerCustomImpl.java
@@ -329,7 +329,14 @@
writer.appendTab2Eol( "] // end property" );
+ // Trace Sequence to cover
+ TraceSpecificationCustomImpl trace =
+ (TraceSpecificationCustomImpl) getTrace();
+ if( trace != null ) {
+ trace.toWriter(writer2);
+ }
+ // Heuristic for trace exploration
writer.appendTab2Eol( "heuristic [" );
if( isOrderedTrace() ) {
@@ -356,13 +363,7 @@
writer.appendTab2Eol( "] // end heuristic" );
-
- TraceSpecificationCustomImpl trace =
- (TraceSpecificationCustomImpl) getTrace();
- if( trace != null ) {
- trace.toWriter(writer2);
- }
-
+ // Console configuration
ConsoleLogFormatCustomImpl console =
(ConsoleLogFormatCustomImpl) getConsole();
if( console != null ) {
diff --git a/execution/org.eclipse.efm.execution.core/src/org/eclipse/efm/execution/core/workflow/serializer/SymbexGraphvizSerializerWorkerCustomImpl.java b/execution/org.eclipse.efm.execution.core/src/org/eclipse/efm/execution/core/workflow/serializer/SymbexGraphvizSerializerWorkerCustomImpl.java
index 4ef0014..3a33c95 100644
--- a/execution/org.eclipse.efm.execution.core/src/org/eclipse/efm/execution/core/workflow/serializer/SymbexGraphvizSerializerWorkerCustomImpl.java
+++ b/execution/org.eclipse.efm.execution.core/src/org/eclipse/efm/execution/core/workflow/serializer/SymbexGraphvizSerializerWorkerCustomImpl.java
@@ -235,24 +235,26 @@
writer2.appendTab2Eol( "data#selection = 'MODIFIED'" );
writer2.appendTabEol( "] // end property" );
- TraceSpecificationCustomImpl format =
- (TraceSpecificationCustomImpl) getFormat();
- if( format != null ) {
- format.toWriter( writer2 );
- }
-
- TraceSpecificationCustomImpl css =
- (TraceSpecificationCustomImpl) getCSS();
- if( css != null ) {
- css.toWriter( writer2 );
- }
-
+ // Trace element selected
TraceSpecificationCustomImpl trace =
(TraceSpecificationCustomImpl) getTrace();
if( trace != null ) {
trace.toWriter(writer2);
}
+ // Trace element formatter
+ TraceSpecificationCustomImpl format =
+ (TraceSpecificationCustomImpl) getFormat();
+ if( format != null ) {
+ format.toWriter( writer2 );
+ }
+
+ // Graphviz node shape, color, ...
+ TraceSpecificationCustomImpl css =
+ (TraceSpecificationCustomImpl) getCSS();
+ if( css != null ) {
+ css.toWriter( writer2 );
+ }
String justifier = "";
String path;
diff --git a/gui/org.eclipse.efm.ui.intro/build.properties b/gui/org.eclipse.efm.ui.intro/build.properties
index 6f20375..f78bc4b 100644
--- a/gui/org.eclipse.efm.ui.intro/build.properties
+++ b/gui/org.eclipse.efm.ui.intro/build.properties
@@ -2,4 +2,6 @@
output.. = bin/
bin.includes = META-INF/,\
.,\
- plugin.xml
+ plugin.xml,\
+ extensions/,\
+ images/
diff --git a/gui/org.eclipse.efm.ui.intro/plugin.xml b/gui/org.eclipse.efm.ui.intro/plugin.xml
index e2090ed..4d0c9a7 100644
--- a/gui/org.eclipse.efm.ui.intro/plugin.xml
+++ b/gui/org.eclipse.efm.ui.intro/plugin.xml
@@ -15,5 +15,21 @@
content="extensions/tutorialsExtensionContent.xml">
</configExtension>
</extension>
+ <extension
+ point="org.eclipse.ui.intro.quicklinks">
+ <command
+ icon="images/efm48.png"
+ id="org.eclipse.efm.execution.launchconfiguration.command.graphviz"
+ importance="high"
+ label="Eclipse Formal Modeling">
+ </command>
+ <url
+ description="A guided walkthrough to the Eclipse Formal Modeling framework"
+ icon="images/efm48.png"
+ importance="high"
+ label="Eclipse Formal Modeling"
+ location="http://org.eclipse.ui.intro/showHelpTopic?id=/org.eclipse.efm.modeling.doc.helpcontents/resources/docs/toc.xml">
+ </url>
+ </extension>
</plugin>
diff --git a/releng/org.eclipse.efm.modeling.rcp/plugin.xml b/releng/org.eclipse.efm.modeling.rcp/plugin.xml
index b77c391..9e6cabe 100644
--- a/releng/org.eclipse.efm.modeling.rcp/plugin.xml
+++ b/releng/org.eclipse.efm.modeling.rcp/plugin.xml
@@ -9,7 +9,7 @@
description="Papyrus

Version: 1.0.0

(c) Copyright Eclipse contributors and others 2000, 2015. All rights reserved.
Visit http://www.eclipse.org/platform

This product includes software developed by the
Apache Software Foundation http://www.apache.org/"
name="Eclipse Formal Modeling & Symbex Tools">
<property name="windowImages" value="icons/efm16.png,icons/efm32.png,icons/efm48.png,icons/efm64.png,icons/efm128.png,icons/efm256.png"/>
- <property name="aboutImage" value="icons/efm128.png"/>
+ <property name="aboutImage" value="icons/efm_lg.png"/>
<property
name="appName"
value="Eclipse Formal Modeling & Symbex Tools">
@@ -47,7 +47,7 @@
</property>
<property
name="aboutText"
- value="Eclipse Formal Modeling (Incubation)

(c) Copyright Eclipse contributors and others 2000, 2016. All rights reserved.
Visit http://www.eclipse.org/platform

This product includes software developed by the
Apache Software Foundation http://www.apache.org/">
+ value="Eclipse Formal Modeling (Incubation)

(c) Copyright Eclipse contributors and others 2000, 2016. All rights reserved.
Visit http://www.eclipse.org/platform

This product includes software developed by the
Apache Software Foundation http://www.apache.org/">
</property>
<property
name="preferenceCustomization"
