Update to 1.7.0 (#477)

p-org · Dec 11, 2019 · 631fcd2 · 631fcd2
1 parent c4f12a9
commit 631fcd2
Show file tree

Hide file tree

Showing 145 changed files with 51 additions and 1,897 deletions.
diff --git a/Common/version.props b/Common/version.props
@@ -1,7 +1,7 @@
 <!-- This file may be overwritten by automation. Only values allowed here are VersionPrefix and VersionSuffix.  -->
 <Project>
   <PropertyGroup>
-    <VersionPrefix>1.6.10</VersionPrefix>
+    <VersionPrefix>1.7.0</VersionPrefix>
     <VersionSuffix></VersionSuffix>
   </PropertyGroup>
 </Project>
diff --git a/Docs/Images/TraceViewer/trace_viewer_0.png b/Docs/Images/TraceViewer/trace_viewer_0.png
diff --git a/Docs/Images/TraceViewer/trace_viewer_1.png b/Docs/Images/TraceViewer/trace_viewer_1.png
diff --git a/Docs/Images/TraceViewer/trace_viewer_2.png b/Docs/Images/TraceViewer/trace_viewer_2.png
diff --git a/Docs/Images/TraceViewer/trace_viewer_3.png b/Docs/Images/TraceViewer/trace_viewer_3.png
diff --git a/Docs/README.md b/Docs/README.md
@@ -30,7 +30,6 @@ Learn how to use the P# testing infrastructure to write unit-tests, thoroughly c
 ## Tools
 The following provides information regarding the available tools in the P# ecosystem:
 - [P# Compiler](Tools/Compiler.md)
-- [P# Trace Viewer](Tools/TraceViewer.md)
 - [P# Race Detector](Tools/RaceDetection.md)
 - [P# Batch Tester](https://github.com/p-org/PSharpBatchTesting)
 

diff --git a/Docs/Tools/TraceViewer.md b/Docs/Tools/TraceViewer.md
diff --git a/Samples/Framework/build.props b/Samples/Framework/build.props
@@ -12,6 +12,6 @@
     <OutputPath>..\bin\</OutputPath>
   </PropertyGroup>
   <ItemGroup>
-    <PackageReference Include="Microsoft.PSharp" Version="1.6.10" />
+    <PackageReference Include="Microsoft.PSharp" Version="1.7.0" />
   </ItemGroup>
 </Project>
diff --git a/Samples/Language/build.props b/Samples/Language/build.props
@@ -10,6 +10,6 @@
     <OutputPath>..\bin\</OutputPath>
   </PropertyGroup>
   <ItemGroup>
-    <PackageReference Include="Microsoft.PSharp" Version="1.6.10" />
+    <PackageReference Include="Microsoft.PSharp" Version="1.7.0" />
   </ItemGroup>
 </Project>
diff --git a/Source/Core/Configuration.cs b/Source/Core/Configuration.cs
@@ -6,8 +6,6 @@
 using System;
 using System.Collections.Generic;
 using System.Runtime.Serialization;
-
-using Microsoft.PSharp.IO;
 using Microsoft.PSharp.Utilities;
 
 namespace Microsoft.PSharp

diff --git a/Source/Core/Properties/InternalsVisibleTo.cs b/Source/Core/Properties/InternalsVisibleTo.cs
@@ -50,12 +50,6 @@
     "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
     "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
     "3bc97f9e")]
-[assembly: InternalsVisibleTo("PSharpTraceViewer,PublicKey=" +
-    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
-    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
-    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
-    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
-    "3bc97f9e")]
 [assembly: InternalsVisibleTo("PSharpSyntaxRewriter,PublicKey=" +
     "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
     "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +

diff --git a/Source/Core/Properties/codeanalysis.ruleset b/Source/Core/Properties/codeanalysis.ruleset
@@ -19,7 +19,7 @@
     <Rule Id="CA1305" Action="None" />
     <Rule Id="CA1307" Action="None" />
     <Rule Id="CA1707" Action="Error" />
-    <Rule Id="CA1710" Action="Error" />
+    <Rule Id="CA1710" Action="None" />
     <Rule Id="CA1715" Action="None" />
     <Rule Id="CA1716" Action="None" />
     <Rule Id="CA1720" Action="None" />

diff --git a/Source/Core/Runtime/Events/EventInfo.cs b/Source/Core/Runtime/Events/EventInfo.cs
@@ -3,7 +3,6 @@
 // Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
 // ------------------------------------------------------------------------------------------------
 
-using System;
 using System.Runtime.Serialization;
 
 using Microsoft.PSharp.Runtime;
@@ -14,19 +13,19 @@ namespace Microsoft.PSharp
     /// Contains an <see cref="Event"/>, and its associated metadata.
     /// </summary>
     [DataContract]
-    internal class EventInfo
+    public class EventInfo
     {
         /// <summary>
         /// Event name.
         /// </summary>
         [DataMember]
-        internal string EventName { get; private set; }
+        public string EventName { get; private set; }
 
         /// <summary>
         /// Information regarding the event origin.
         /// </summary>
         [DataMember]
-        internal EventOriginInfo OriginInfo { get; private set; }
+        public EventOriginInfo OriginInfo { get; private set; }
 
         /// <summary>
         /// True if this event must always be handled, else false.

diff --git a/Source/Core/Runtime/Events/EventOriginInfo.cs b/Source/Core/Runtime/Events/EventOriginInfo.cs
@@ -11,25 +11,25 @@ namespace Microsoft.PSharp.Runtime
     /// Contains the origin information of an <see cref="Event"/>.
     /// </summary>
     [DataContract]
-    internal class EventOriginInfo
+    public class EventOriginInfo
     {
         /// <summary>
         /// The sender machine id.
         /// </summary>
         [DataMember]
-        internal MachineId SenderMachineId { get; private set; }
+        public MachineId SenderMachineId { get; private set; }
 
         /// <summary>
         /// The sender machine name.
         /// </summary>
         [DataMember]
-        internal string SenderMachineName { get; private set; }
+        public string SenderMachineName { get; private set; }
 
         /// <summary>
         /// The sender machine state name.
         /// </summary>
         [DataMember]
-        internal string SenderStateName { get; private set; }
+        public string SenderStateName { get; private set; }
 
         /// <summary>
         /// Initializes a new instance of the <see cref="EventOriginInfo"/> class.

diff --git a/Source/DataFlowAnalysis/Graphs/Graph.cs b/Source/DataFlowAnalysis/Graphs/Graph.cs
@@ -3,7 +3,6 @@
 // Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
 // ------------------------------------------------------------------------------------------------
 
-using System;
 using System.Collections.Generic;
 using System.Linq;
 

diff --git a/Source/DataFlowAnalysis/Graphs/IGraph.cs b/Source/DataFlowAnalysis/Graphs/IGraph.cs
@@ -3,9 +3,7 @@
 // Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
 // ------------------------------------------------------------------------------------------------
 
-using System;
 using System.Collections.Generic;
-using System.Linq;
 
 namespace Microsoft.PSharp.DataFlowAnalysis
 {

diff --git a/Source/DataFlowAnalysis/Properties/codeanalysis.ruleset b/Source/DataFlowAnalysis/Properties/codeanalysis.ruleset
@@ -19,7 +19,7 @@
     <Rule Id="CA1305" Action="None" />
     <Rule Id="CA1307" Action="None" />
     <Rule Id="CA1707" Action="Error" />
-    <Rule Id="CA1710" Action="Error" />
+    <Rule Id="CA1710" Action="None" />
     <Rule Id="CA1715" Action="None" />
     <Rule Id="CA1716" Action="None" />
     <Rule Id="CA1720" Action="None" />

diff --git a/Source/LanguageServices/Exceptions/ParsingException.cs b/Source/LanguageServices/Exceptions/ParsingException.cs
@@ -4,8 +4,6 @@
 // ------------------------------------------------------------------------------------------------
 
 using System;
-using System.Collections.Generic;
-using System.Linq;
 
 using Microsoft.PSharp.LanguageServices.Parsing;
 

diff --git a/Source/LanguageServices/Parsing/Visitors/Syntax/Declarations/StateGroupDeclarationVisitor.cs b/Source/LanguageServices/Parsing/Visitors/Syntax/Declarations/StateGroupDeclarationVisitor.cs
@@ -3,7 +3,6 @@
 // Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
 // ------------------------------------------------------------------------------------------------
 
-using Microsoft.CodeAnalysis.CSharp.Syntax;
 using Microsoft.PSharp.LanguageServices.Syntax;
 
 namespace Microsoft.PSharp.LanguageServices.Parsing.Syntax

diff --git a/Source/LanguageServices/Properties/codeanalysis.ruleset b/Source/LanguageServices/Properties/codeanalysis.ruleset
@@ -19,7 +19,7 @@
     <Rule Id="CA1305" Action="None" />
     <Rule Id="CA1307" Action="None" />
     <Rule Id="CA1707" Action="Error" />
-    <Rule Id="CA1710" Action="Error" />
+    <Rule Id="CA1710" Action="None" />
     <Rule Id="CA1715" Action="None" />
     <Rule Id="CA1716" Action="None" />
     <Rule Id="CA1720" Action="None" />

diff --git a/Source/LanguageServices/Rewriting/PSharp/PSharpRewriter.cs b/Source/LanguageServices/Rewriting/PSharp/PSharpRewriter.cs
@@ -3,13 +3,6 @@
 // Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
 // ------------------------------------------------------------------------------------------------
 
-using System.Linq;
-
-using Microsoft.CodeAnalysis;
-using Microsoft.CodeAnalysis.CSharp.Syntax;
-
-using Microsoft.PSharp.LanguageServices.Syntax;
-
 namespace Microsoft.PSharp.LanguageServices.Rewriting.PSharp
 {
     /// <summary>

diff --git a/Source/LanguageServices/Syntax/Declarations/StateGroupDeclaration.cs b/Source/LanguageServices/Syntax/Declarations/StateGroupDeclaration.cs
@@ -8,7 +8,6 @@
 
 using Microsoft.PSharp.IO;
 using Microsoft.PSharp.LanguageServices.Parsing;
-using Microsoft.PSharp.LanguageServices.Rewriting.PSharp;
 
 namespace Microsoft.PSharp.LanguageServices.Syntax
 {

diff --git a/Source/SharedObjects/Properties/codeanalysis.ruleset b/Source/SharedObjects/Properties/codeanalysis.ruleset
@@ -19,7 +19,7 @@
     <Rule Id="CA1305" Action="None" />
     <Rule Id="CA1307" Action="None" />
     <Rule Id="CA1707" Action="Error" />
-    <Rule Id="CA1710" Action="Error" />
+    <Rule Id="CA1710" Action="None" />
     <Rule Id="CA1715" Action="None" />
     <Rule Id="CA1716" Action="None" />
     <Rule Id="CA1720" Action="None" />

diff --git a/Source/StaticAnalysis/Properties/codeanalysis.ruleset b/Source/StaticAnalysis/Properties/codeanalysis.ruleset
@@ -19,7 +19,7 @@
     <Rule Id="CA1305" Action="None" />
     <Rule Id="CA1307" Action="None" />
     <Rule Id="CA1707" Action="Error" />
-    <Rule Id="CA1710" Action="Error" />
+    <Rule Id="CA1710" Action="None" />
     <Rule Id="CA1715" Action="None" />
     <Rule Id="CA1716" Action="None" />
     <Rule Id="CA1720" Action="None" />

diff --git a/Source/StaticAnalysis/Summarization/StateMachines/OnEntryMachineAction.cs b/Source/StaticAnalysis/Summarization/StateMachines/OnEntryMachineAction.cs
@@ -4,7 +4,6 @@
 // ------------------------------------------------------------------------------------------------
 
 using Microsoft.CodeAnalysis.CSharp.Syntax;
-using Microsoft.PSharp.DataFlowAnalysis;
 
 namespace Microsoft.PSharp.StaticAnalysis
 {

diff --git a/Source/StaticAnalysis/Summarization/StateMachines/OnEventDoMachineAction.cs b/Source/StaticAnalysis/Summarization/StateMachines/OnEventDoMachineAction.cs
@@ -4,7 +4,6 @@
 // ------------------------------------------------------------------------------------------------
 
 using Microsoft.CodeAnalysis.CSharp.Syntax;
-using Microsoft.PSharp.DataFlowAnalysis;
 
 namespace Microsoft.PSharp.StaticAnalysis
 {

diff --git a/Source/StaticAnalysis/Summarization/StateMachines/OnEventGotoMachineAction.cs b/Source/StaticAnalysis/Summarization/StateMachines/OnEventGotoMachineAction.cs
@@ -4,7 +4,6 @@
 // ------------------------------------------------------------------------------------------------
 
 using Microsoft.CodeAnalysis.CSharp.Syntax;
-using Microsoft.PSharp.DataFlowAnalysis;
 
 namespace Microsoft.PSharp.StaticAnalysis
 {

diff --git a/Source/StaticAnalysis/Summarization/StateMachines/OnEventPushMachineAction.cs b/Source/StaticAnalysis/Summarization/StateMachines/OnEventPushMachineAction.cs
@@ -4,7 +4,6 @@
 // ------------------------------------------------------------------------------------------------
 
 using Microsoft.CodeAnalysis.CSharp.Syntax;
-using Microsoft.PSharp.DataFlowAnalysis;
 
 namespace Microsoft.PSharp.StaticAnalysis
 {

diff --git a/Source/StaticAnalysis/Summarization/StateMachines/OnExitMachineAction.cs b/Source/StaticAnalysis/Summarization/StateMachines/OnExitMachineAction.cs
@@ -4,7 +4,6 @@
 // ------------------------------------------------------------------------------------------------
 
 using Microsoft.CodeAnalysis.CSharp.Syntax;
-using Microsoft.PSharp.DataFlowAnalysis;
 
 namespace Microsoft.PSharp.StaticAnalysis
 {

diff --git a/Source/StaticAnalysis/Tracing/TraceInfo.cs b/Source/StaticAnalysis/Tracing/TraceInfo.cs
@@ -3,7 +3,6 @@
 // Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
 // ------------------------------------------------------------------------------------------------
 
-using System;
 using System.Collections.Generic;
 
 using Microsoft.CodeAnalysis;

diff --git a/Source/TestingServices/Engines/ITestingEngine.cs b/Source/TestingServices/Engines/ITestingEngine.cs
@@ -4,7 +4,6 @@
 // ------------------------------------------------------------------------------------------------
 
 using System;
-using Microsoft.PSharp.IO;
 
 namespace Microsoft.PSharp.TestingServices
 {

diff --git a/Source/TestingServices/Events/QuiescentEvent.cs b/Source/TestingServices/Events/QuiescentEvent.cs
@@ -3,7 +3,6 @@
 // Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
 // ------------------------------------------------------------------------------------------------
 
-using System;
 using System.Runtime.Serialization;
 
 namespace Microsoft.PSharp

diff --git a/Source/TestingServices/Properties/InternalsVisibleTo.cs b/Source/TestingServices/Properties/InternalsVisibleTo.cs
@@ -32,12 +32,6 @@
     "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
     "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
     "3bc97f9e")]
-[assembly: InternalsVisibleTo("PSharpTraceViewer,PublicKey=" +
-    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
-    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
-    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
-    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
-    "3bc97f9e")]
 [assembly: InternalsVisibleTo("PSharpTestLauncher,PublicKey=" +
     "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
     "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +

diff --git a/Source/TestingServices/Properties/codeanalysis.ruleset b/Source/TestingServices/Properties/codeanalysis.ruleset
@@ -19,7 +19,7 @@
     <Rule Id="CA1305" Action="None" />
     <Rule Id="CA1307" Action="None" />
     <Rule Id="CA1707" Action="Error" />
-    <Rule Id="CA1710" Action="Error" />
+    <Rule Id="CA1710" Action="None" />
     <Rule Id="CA1715" Action="None" />
     <Rule Id="CA1716" Action="None" />
     <Rule Id="CA1720" Action="None" />

diff --git a/Source/TestingServices/Tracing/Error/BugTrace.cs b/Source/TestingServices/Tracing/Error/BugTrace.cs
@@ -16,7 +16,7 @@ namespace Microsoft.PSharp.TestingServices.Tracing.Error
     /// some end state.
     /// </summary>
     [DataContract]
-    internal sealed class BugTrace : IEnumerable, IEnumerable<BugTraceStep>
+    public sealed class BugTrace : IEnumerable, IEnumerable<BugTraceStep>
     {
         /// <summary>
         /// The steps of the bug trace.
@@ -27,15 +27,15 @@ internal sealed class BugTrace : IEnumerable, IEnumerable<BugTraceStep>
         /// <summary>
         /// The number of steps in the bug trace.
         /// </summary>
-        internal int Count
+        public int Count
         {
             get { return this.Steps.Count; }
         }
 
         /// <summary>
         /// Index for the bug trace.
         /// </summary>
-        internal BugTraceStep this[int index]
+        public BugTraceStep this[int index]
         {
             get { return this.Steps[index]; }
             set { this.Steps[index] = value; }
@@ -212,6 +212,7 @@ internal BugTraceStep Peek()
         /// <summary>
         /// Returns an enumerator.
         /// </summary>
+        /// <returns>The enumerator.</returns>
         IEnumerator IEnumerable.GetEnumerator()
         {
             return this.Steps.GetEnumerator();
@@ -220,6 +221,7 @@ IEnumerator IEnumerable.GetEnumerator()
         /// <summary>
         /// Returns an enumerator.
         /// </summary>
+        /// <returns>The enumerator.</returns>
         IEnumerator<BugTraceStep> IEnumerable<BugTraceStep>.GetEnumerator()
         {
             return this.Steps.GetEnumerator();