Spec Explorer Release Notes

Article
07/08/2013

For Spec Explorer 3.5.3146.0.

What’s New in Spec Explorer 2010 Release 3.5.3146.0

Support for Visual Studio 2012
Model change detecting
Multiple machine processing
Cord context menu

Spec Explorer 2010 Release 3.5.3146.0 runs only on Visual Studio 2010 and Visual Studio 2012. It does not work with Visual Studio 2008. Please see the notes in the Installation section of this document.

You can find additional details about these changes and other feature enhancements in the section below entitled “Overview of New and Enhanced Features”.

Availability

Spec Explorer is a Visual Studio Power Tool. Its Home Page is on the Visual Studio Gallery.

System Requirements

1 gigahertz (GHz) Pentium processor or greater recommended
Windows XP (x86) with Service Pack 3, Windows Vista (x86 & x64) with Service Pack 2, Windows 7 (x86 & x64), Windows 8 (x86 & x64), Windows Server 2003 (x86 & x64) with Service Pack 2, Windows Server 2003 R2 (x86 & x64), Windows Server 2008 (x86 & x64) with Service Pack 2, Windows Server 2008 R2 (x64).
1 GB or greater RAM (2 GB recommended)
70 MB of available space on system drive
Professional / Premium / Ultimate edition of Microsoft Visual Studio® 2010 or 2012

Installation

A successful installation will add “Spec Explorer” to the top level command menu of Visual Studio 2010 and a “Spec Explorer 2010” entry to the Windows Start menu. All instances of Visual Studio should be closed before installing Spec Explorer.

It is no longer possible to install this or future versions of Spec Explorer 2010 on Visual Studio 2008 or any pre-release versions of Visual Studio 2010.

SpecExplorer.exe

SpecExplorer.exe runs as a standalone command-line tool and is installed at the same time as the Spec Explorer add-in for Visual Studio 2010. To deploy SpecExplorer.exe to an automation environment without Visual Studio, copy the entire contents of the installation directory with subdirectories.

Further Documentation and Assistance

Documentation can be obtained from the following sources:

Spec Explorer on-line Help can be found in Spec Explorer MSDN site.
Spec Explorer 2010 local Help is available via the Windows Start menu at: All Programs-> Spec Explorer 2010->Spec Explorer 2010 Documentation.
The Spec Explorer code samples are available via the Windows Start menu at: All Programs->Spec Explorer 2010-> Samples for Visual Studio 2010.
The Spec Explorer Forum can be found here.
The Spec Explorer Blog can be found here.

Overview of New and Enhanced Features

The following features have been added or enhanced in this release:

Model change detecting
Multiple machine processing
Cord context menu

Enhanced Feature: Model Change Detecting

The model change detecting feature detects all model changes and decides if Spec Explorer needs to re-explore the model. For specific machines, if Spec Explorer detects any change in the model code, cord script files, or other inputs, or detects a tool version change, Spec Explorer will start a new exploration; otherwise, Spec Explorer will use existing exploration result files for current exploration viewing, test code generation, and user customized post processing. The UI has been updated to allow you to force Spec Explorer to re-explore the machines. This feature greatly improves the user experience by preventing unneeded lengthy validation and exploration events, which frequently happened in previous versions.

Enhanced Feature: Multiple Machine Processing

Now you can select multiple machines in Exploration Manager and explore, generate test code, or perform post processing tasks on them. For multiple machine processing, Spec Explorer generates a summary including all information of the batch-processing.Hot keys for multi-selection such as Ctrl+A, Shift and Ctrl selection are also supported.The button and context menu item of “Generate Test Code for All” has been removed.

Spec Explorer adds a new context menu item “Go To Definition” in the Cord editor, which enables users to navigate to specific configurations and machines. This is part of an ongoing effort to improve the Cord editing user experience and the general integration of the tool with Visual Studio.Hot key F12 is also supported.

Managing Help Documentation

For help documentation, Spec Explorer uses the Help Viewer and the Help Library Manager (HLM). As an extension to Visual Studio, Spec Explorer relies on Visual Studio for access to the HLM which configures the help system and is available in the Visual Studio Help menu by choosing Manage Help Settings. The HLM allows you to determine where to obtain the help that you might later request when using Spec Explorer. You can select whether you want the help system to direct help requests to the online content or to a local copy of the content. This flexible system allows you to easily switch help access to better match when usage is online or offline. The HLM also allows online updates to the documentation to be downloaded to a computer for local use by Spec Explorer.

In HLM the Install Content from Disk dialog can be used to browse to the HelpContent directory and select file HelpContentSetup.msha to manually direct the help system to use the pre-installed, locally-resident copy of the help content. This default copy of the documentation is a snapshot of the content at the time of release. When relying on the local help, it is recommended that you go online and request the HLM to download and update the local copy of the documentation.

The most recently updated documentation is found in the online content. When online help access is chosen in the HLM, the help system automatically directs requests for help to the online content. Using a direct link is not required. There may occasionally be short periods of time when the online content has been updated but the changes have not yet been propagated to the offline content.

Known Outstanding Issues

The following issues are known to be outstanding in this release of Spec Explorer.

If you do not have VS2010 installed on your machine, you need to install the VC++9.0 redistributable package before installing SE. You can find the package here: https://www.microsoft.com/en-us/download/details.aspx?id=5582.
When opening the SMB2 sample project with VS2012, VS will prompt for upgrading one of the projects. Please allow the upgrade, otherwise the project will not compile.
You cannot run the generated test code for the AtSvc sample on Windows 8 machines because the “at.exe” command has been removed. However, you should be able to explore the model and generate test code.

Constructs applied to behaviors with multiple initial states can yield unexpected results: Constructing test cases, requirement coverage, dead path elimination, accept completion, or point & shoot for behaviors with more than one state containing different values or constraints is not advised, as the resulting behavior is likely to be different than expected.

A typical scenario is using ‘let’ declarations in Cord to expand variables before the first step in a behavior:

machine ExpandedDoubleAdd() : Main where ForExploration = true
{
    (
        let int x, int y where 
            {.
               Condition.In(x, 1, 2); 
               Condition.In(y, 1, 2, 3);
               Combination.Interaction(x);
               Combination.Interaction(y);
               Combination.Expand(x,y);
            .} 
        in 
            Add (x); 
            Add(y);
    )
    ||
    (construct model program from Main) 
}

Since variables x and y will be expanded in the initial state, there will be several initial states with different values for these variables. Constructing test cases for machine “ExpandedDoubleAdd” will result in unexpected non-accepting states.

Work-around: One way to prevent this problem is to introduce a “no-operation” action to expand the parameters, so that the expansion occurs in a step, rather than in the initial state. This new action will appear in test cases, but should have an empty implementation in the test adapter.

For the example above, a new action, NoOp would be introduced in the Cord config:

config Main 
{
   …
       action abstract static void Implementation.NoOp(int x, int y); 
   …
}

Then a rule method would be declared in the model program for action NoOp containing the parameter expansion and interactions:

[Action]
      static void NoOp(int x, int y)
      {
             Combination.Interaction(x);
             Combination.Interaction(y);
             Combination.Expand(x, y);
      }

The interactions and expansion would then be removed from the Cord script and replaced with an invocation of the new action:

machine ExpandedDoubleAdd() : Main where ForExploration = true
{
       (
           let int x, int y where 
           {.
               Condition.In(x, 1, 2); 
               Condition.In(y, 1, 2, 3);
           .} 
           in
             NoOp(x,y); 
             Add (x); 
             Add(y);
       )
    ||
       (construct model program from Main)
}

The new ExpandedDoubleAdd machine will have a single initial state and will thus be suitable to be applied to a construct:

machine DoubleAddTestSuite(): Main where ForExploration = true,
 TestEnabled = true
{
       construct test cases where Strategy= "ShortTests" for 
         ExpandedDoubleAdd
}

Cannot save image of large exploration graph: It is not possible to save the image of a large exploration graph of approximately 9000 by 7000 pixels or more. This is due to the current viewer component used by Spec Explorer.

Work-around: None
Exploration graph is too big: Sometimes VS may stop working when rendering the graph. Also, the viewer may not wait long enough even when the RenderingTimeOut switch is specified.

Work-around: None
Exceptions not supported for testing: Exceptions cannot be the expected results of actions in this release. If an exception is raised by a system under test or test adapter, it results in a test failure.

Work-around: Catch the exception in the adapter and return a value indicating to the model that the operation has failed.
Typed Domain: Object domain definitions similar to “domain object = (. DomainGenerator .)” are not supported.

Work-around: None
Structs and parameter generation: Unexpected interactions can result from applying the Expand and ExcludeFromExpansion methods to struct fields, for example:
- Applying the Expand method to a field of a struct has no effect. The field is not expanded and remains symbolic.
- Applying the ExcludeFromExpansion method to a field of a struct has no effect. The field is still expanded if it has a domain.
Work-around: None
Logical operators in the combination API: Do not use a logical AND (&&), logical OR (||), the conditional operator (?:), CompoundValue, or object field selection on Combination.Seeded or Combination.Isolated because they can generate additional branches that are not expected.

Work-around: For logical operators, use bitwise operators instead. Try to expand CompoundValue or objects before accessing their fields and avoid using conditional operators.
Error state aborts traversal: For behaviors that contain error states, Spec Explorer cannot apply the test case traversal, dead path elimination, or requirement coverage constructs.

Work-around: None
C# collection initializers and immutable collections: Mutable collections such as the SequenceContainer, SetContainer, and MapContainer classes can utilize the C# collection initialization syntax, as follows:
```
SetContainer<int> set = new SetContainer<int>{1, 3, 5};
```
Immutable collections such as Sequence, Set, and Map cannot use collection initialization syntax as shown because C# would translate it into several calls to the Add method (which does not change the collection). The collection would be empty, and no error message would be displayed.

Work-around: The following syntax must be used to initialize an immutable collection (using parenthesis, instead of braces):
```
Set<int> set = new Set<int>(1, 3, 5);
```
Exploration results in an error state with description “Constraint solver exceeded configured time bound”: Spec Explorer relies on an underlying constraint solver for generating parameters of actions as well as deciding whether a rule can be enabled or not. The solver algorithm is highly heuristic and sometimes may fail to provide a solution within a specific time bound.

Work-around: Try increasing the time bound by setting the “ConstraintSolverTimeout” switch in the Cord config.
Offline Help Library cannot be installed successfully on x64 platform until user chooses to sync from online document: Installing Spec Explorer on x86 and x64 machines results in the same exploration / test case generation behavior; but the offline help library cannot be installed successfully on the x64 platform.

Work-around: Synchcronize from online documents manually.
Spec Explorer cannot explore a machine correctly when the model project is extracted from a downloaded ZIP file: When exploring a machine after unzipping a downloaded model project, sometimes you can see errors like:

fatal execution failure: Could not load file or assembly 'file:///D:\ \SpecExplorer6\bin\Debug\SpecExplorer6.dll' or one of its dependencies. Operation is not supported. (Exception from HRESULT: 0x80131515)

An attempt was made to load an assembly from a network location which would have caused the assembly to be sandboxed in previous versions of the .NET Framework. This release of the .NET Framework does not enable CAS policy by default, so this load may be dangerous. If this load is not intended to sandbox the assembly, please enable the loadFromRemoteSources switch. See https://go.microsoft.com/fwlink/?LinkId=155569 for more information.

**Work-around:**Windows treats downloaded zip files and their contensts as untrusted. There are two work-arounds:
1. Click the “Unblock” button in the properties of the ZIP files or the corresponding DLL files. Or:
2. Configure attachment management group policy
  - In Windows, Click Start.
  - In the Search box, Run box or console window type: GPEDIT.MSC to bring up the Group Policy Object (GPO) editor.
  - Navigate to User Configuration > Administrative Templates > Windows Components > Attachment Manager. ENABLE the policy called "Do not preserve zone information in file attachments".
  - Close the GPO editor.
  - Either logoff your computer, or refresh the local policy by typing the following command in a Command Prompt or in the Run box: Gpupdate /force
Cannot find Spec Explorer in Program list when another user has installed Spec Explorer: Spec Explorer is installed for individual users instead of for all users. All samples are installed in the corresponding user document folder.

Work-around: Install Spec Explorer again for current user.
Cannot modify the Spec Explorer TestSuite project target framework: You cannot change the specified .NET framework version or profile for a test project in Visual Studio 2010.

Work-around: Create a new test project using the specified .NET framework.

Breaking/Important Changes

Breaking changes:

The TestFailureException class has been moved from the Microsoft.SpecExplorer.Runtime namespace to Microsoft.SpecExplorer.Runtime.Testing. If you are using the Dynamic Traversal feature, and are processing the TestFailureException, you should change the namespace in the using directive.
Added the AlwaysReexplore property to the IMachine interface. If you customize your own machine extension by implementing the IMachine interface, you can set this property to false to benefit from model change detecting feature; or set this property to true, so Spec Explorer will always re-explore the corresponding machine.
The button and the context menu item for “Generate Test Code for All” have been removed.
Deprecated switch “Namespace” is removed, use “Scope” instead.
Deprecated switch “IncludeSystem” is removed.

Important changes:

All samples are updated to enable on-the-fly testing, note that on-the-fly testing does not rely on project dependencies, use the fully qualified name when declaring the base test class.
The Spec Explorer document has been improved to contain more detailed information on reference pages.

Bugs Fixed

Over 60 bugs have been fixed in this release including:

On-The-Fly Testing no longer intermittently crashes when the Stop button is pushed.
On-The-Fly Testing is now available through the SpecExplorer.exe command line tool.
Crashing issue when sorting a list by a nullable type has been fixed.
The issue of incorrect test code generation when using collections with inheritance has been fixed.
The issue of stack overflow when returning a native delegate has been fixed.
All samples were refined to enable On-The-Fly Testing.