Skip to content
This repository was archived by the owner on Aug 26, 2022. It is now read-only.

Commit 631fcd2

Browse files
pdeligiapdeligia
authored
Update to 1.7.0 (#477)
1 parent c4f12a9 commit 631fcd2

File tree

145 files changed

+51
-1897
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

145 files changed

+51
-1897
lines changed

‎Common/version.props

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
<!-- This file may be overwritten by automation. Only values allowed here are VersionPrefix and VersionSuffix. -->
22
<Project>
33
<PropertyGroup>
4-
<VersionPrefix>1.6.10</VersionPrefix>
4+
<VersionPrefix>1.7.0</VersionPrefix>
55
<VersionSuffix></VersionSuffix>
66
</PropertyGroup>
77
</Project>

‎Docs/Images/TraceViewer/trace_viewer_0.png

-178 KB
Binary file not shown.

‎Docs/Images/TraceViewer/trace_viewer_1.png

-172 KB
Binary file not shown.

‎Docs/Images/TraceViewer/trace_viewer_2.png

-167 KB
Binary file not shown.

‎Docs/Images/TraceViewer/trace_viewer_3.png

-103 KB
Binary file not shown.

‎Docs/README.md

-1
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,6 @@ Learn how to use the P# testing infrastructure to write unit-tests, thoroughly c
3030
## Tools
3131
The following provides information regarding the available tools in the P# ecosystem:
3232
- [P# Compiler](Tools/Compiler.md)
33-
- [P# Trace Viewer](Tools/TraceViewer.md)
3433
- [P# Race Detector](Tools/RaceDetection.md)
3534
- [P# Batch Tester](https://github.com/p-org/PSharpBatchTesting)
3635

‎Docs/Tools/TraceViewer.md

-34
This file was deleted.

‎Samples/Framework/build.props

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,6 @@
1212
<OutputPath>..\bin\</OutputPath>
1313
</PropertyGroup>
1414
<ItemGroup>
15-
<PackageReference Include="Microsoft.PSharp" Version="1.6.10" />
15+
<PackageReference Include="Microsoft.PSharp" Version="1.7.0" />
1616
</ItemGroup>
1717
</Project>

‎Samples/Language/build.props

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,6 @@
1010
<OutputPath>..\bin\</OutputPath>
1111
</PropertyGroup>
1212
<ItemGroup>
13-
<PackageReference Include="Microsoft.PSharp" Version="1.6.10" />
13+
<PackageReference Include="Microsoft.PSharp" Version="1.7.0" />
1414
</ItemGroup>
1515
</Project>

‎Source/Core/Configuration.cs

-2
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,6 @@
66
using System;
77
using System.Collections.Generic;
88
using System.Runtime.Serialization;
9-
10-
using Microsoft.PSharp.IO;
119
using Microsoft.PSharp.Utilities;
1210

1311
namespace Microsoft.PSharp

‎Source/Core/Properties/InternalsVisibleTo.cs

-6
Original file line numberDiff line numberDiff line change
@@ -50,12 +50,6 @@
5050
"d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
5151
"ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
5252
"3bc97f9e")]
53-
[assembly: InternalsVisibleTo("PSharpTraceViewer,PublicKey=" +
54-
"0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
55-
"53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
56-
"d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
57-
"ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
58-
"3bc97f9e")]
5953
[assembly: InternalsVisibleTo("PSharpSyntaxRewriter,PublicKey=" +
6054
"0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
6155
"53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +

‎Source/Core/Properties/codeanalysis.ruleset

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@
1919
<Rule Id="CA1305" Action="None" />
2020
<Rule Id="CA1307" Action="None" />
2121
<Rule Id="CA1707" Action="Error" />
22-
<Rule Id="CA1710" Action="Error" />
22+
<Rule Id="CA1710" Action="None" />
2323
<Rule Id="CA1715" Action="None" />
2424
<Rule Id="CA1716" Action="None" />
2525
<Rule Id="CA1720" Action="None" />

‎Source/Core/Runtime/Events/EventInfo.cs

+3-4
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33
// Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
44
// ------------------------------------------------------------------------------------------------
55

6-
using System;
76
using System.Runtime.Serialization;
87

98
using Microsoft.PSharp.Runtime;
@@ -14,19 +13,19 @@ namespace Microsoft.PSharp
1413
/// Contains an <see cref="Event"/>, and its associated metadata.
1514
/// </summary>
1615
[DataContract]
17-
internal class EventInfo
16+
public class EventInfo
1817
{
1918
/// <summary>
2019
/// Event name.
2120
/// </summary>
2221
[DataMember]
23-
internal string EventName { get; private set; }
22+
public string EventName { get; private set; }
2423

2524
/// <summary>
2625
/// Information regarding the event origin.
2726
/// </summary>
2827
[DataMember]
29-
internal EventOriginInfo OriginInfo { get; private set; }
28+
public EventOriginInfo OriginInfo { get; private set; }
3029

3130
/// <summary>
3231
/// True if this event must always be handled, else false.

‎Source/Core/Runtime/Events/EventOriginInfo.cs

+4-4
Original file line numberDiff line numberDiff line change
@@ -11,25 +11,25 @@ namespace Microsoft.PSharp.Runtime
1111
/// Contains the origin information of an <see cref="Event"/>.
1212
/// </summary>
1313
[DataContract]
14-
internal class EventOriginInfo
14+
public class EventOriginInfo
1515
{
1616
/// <summary>
1717
/// The sender machine id.
1818
/// </summary>
1919
[DataMember]
20-
internal MachineId SenderMachineId { get; private set; }
20+
public MachineId SenderMachineId { get; private set; }
2121

2222
/// <summary>
2323
/// The sender machine name.
2424
/// </summary>
2525
[DataMember]
26-
internal string SenderMachineName { get; private set; }
26+
public string SenderMachineName { get; private set; }
2727

2828
/// <summary>
2929
/// The sender machine state name.
3030
/// </summary>
3131
[DataMember]
32-
internal string SenderStateName { get; private set; }
32+
public string SenderStateName { get; private set; }
3333

3434
/// <summary>
3535
/// Initializes a new instance of the <see cref="EventOriginInfo"/> class.

‎Source/DataFlowAnalysis/Graphs/Graph.cs

-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33
// Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
44
// ------------------------------------------------------------------------------------------------
55

6-
using System;
76
using System.Collections.Generic;
87
using System.Linq;
98

‎Source/DataFlowAnalysis/Graphs/IGraph.cs

-2
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,7 @@
33
// Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
44
// ------------------------------------------------------------------------------------------------
55

6-
using System;
76
using System.Collections.Generic;
8-
using System.Linq;
97

108
namespace Microsoft.PSharp.DataFlowAnalysis
119
{

‎Source/DataFlowAnalysis/Properties/codeanalysis.ruleset

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@
1919
<Rule Id="CA1305" Action="None" />
2020
<Rule Id="CA1307" Action="None" />
2121
<Rule Id="CA1707" Action="Error" />
22-
<Rule Id="CA1710" Action="Error" />
22+
<Rule Id="CA1710" Action="None" />
2323
<Rule Id="CA1715" Action="None" />
2424
<Rule Id="CA1716" Action="None" />
2525
<Rule Id="CA1720" Action="None" />

‎Source/LanguageServices/Exceptions/ParsingException.cs

-2
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,6 @@
44
// ------------------------------------------------------------------------------------------------
55

66
using System;
7-
using System.Collections.Generic;
8-
using System.Linq;
97

108
using Microsoft.PSharp.LanguageServices.Parsing;
119

‎Source/LanguageServices/Parsing/Visitors/Syntax/Declarations/StateGroupDeclarationVisitor.cs

-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33
// Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
44
// ------------------------------------------------------------------------------------------------
55

6-
using Microsoft.CodeAnalysis.CSharp.Syntax;
76
using Microsoft.PSharp.LanguageServices.Syntax;
87

98
namespace Microsoft.PSharp.LanguageServices.Parsing.Syntax

‎Source/LanguageServices/Properties/codeanalysis.ruleset

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@
1919
<Rule Id="CA1305" Action="None" />
2020
<Rule Id="CA1307" Action="None" />
2121
<Rule Id="CA1707" Action="Error" />
22-
<Rule Id="CA1710" Action="Error" />
22+
<Rule Id="CA1710" Action="None" />
2323
<Rule Id="CA1715" Action="None" />
2424
<Rule Id="CA1716" Action="None" />
2525
<Rule Id="CA1720" Action="None" />

‎Source/LanguageServices/Rewriting/PSharp/PSharpRewriter.cs

-7
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,6 @@
33
// Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
44
// ------------------------------------------------------------------------------------------------
55

6-
using System.Linq;
7-
8-
using Microsoft.CodeAnalysis;
9-
using Microsoft.CodeAnalysis.CSharp.Syntax;
10-
11-
using Microsoft.PSharp.LanguageServices.Syntax;
12-
136
namespace Microsoft.PSharp.LanguageServices.Rewriting.PSharp
147
{
158
/// <summary>

‎Source/LanguageServices/Syntax/Declarations/StateGroupDeclaration.cs

-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@
88

99
using Microsoft.PSharp.IO;
1010
using Microsoft.PSharp.LanguageServices.Parsing;
11-
using Microsoft.PSharp.LanguageServices.Rewriting.PSharp;
1211

1312
namespace Microsoft.PSharp.LanguageServices.Syntax
1413
{

‎Source/SharedObjects/Properties/codeanalysis.ruleset

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@
1919
<Rule Id="CA1305" Action="None" />
2020
<Rule Id="CA1307" Action="None" />
2121
<Rule Id="CA1707" Action="Error" />
22-
<Rule Id="CA1710" Action="Error" />
22+
<Rule Id="CA1710" Action="None" />
2323
<Rule Id="CA1715" Action="None" />
2424
<Rule Id="CA1716" Action="None" />
2525
<Rule Id="CA1720" Action="None" />

‎Source/StaticAnalysis/Properties/codeanalysis.ruleset

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@
1919
<Rule Id="CA1305" Action="None" />
2020
<Rule Id="CA1307" Action="None" />
2121
<Rule Id="CA1707" Action="Error" />
22-
<Rule Id="CA1710" Action="Error" />
22+
<Rule Id="CA1710" Action="None" />
2323
<Rule Id="CA1715" Action="None" />
2424
<Rule Id="CA1716" Action="None" />
2525
<Rule Id="CA1720" Action="None" />

‎Source/StaticAnalysis/Summarization/StateMachines/OnEntryMachineAction.cs

-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@
44
// ------------------------------------------------------------------------------------------------
55

66
using Microsoft.CodeAnalysis.CSharp.Syntax;
7-
using Microsoft.PSharp.DataFlowAnalysis;
87

98
namespace Microsoft.PSharp.StaticAnalysis
109
{

‎Source/StaticAnalysis/Summarization/StateMachines/OnEventDoMachineAction.cs

-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@
44
// ------------------------------------------------------------------------------------------------
55

66
using Microsoft.CodeAnalysis.CSharp.Syntax;
7-
using Microsoft.PSharp.DataFlowAnalysis;
87

98
namespace Microsoft.PSharp.StaticAnalysis
109
{

‎Source/StaticAnalysis/Summarization/StateMachines/OnEventGotoMachineAction.cs

-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@
44
// ------------------------------------------------------------------------------------------------
55

66
using Microsoft.CodeAnalysis.CSharp.Syntax;
7-
using Microsoft.PSharp.DataFlowAnalysis;
87

98
namespace Microsoft.PSharp.StaticAnalysis
109
{

‎Source/StaticAnalysis/Summarization/StateMachines/OnEventPushMachineAction.cs

-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@
44
// ------------------------------------------------------------------------------------------------
55

66
using Microsoft.CodeAnalysis.CSharp.Syntax;
7-
using Microsoft.PSharp.DataFlowAnalysis;
87

98
namespace Microsoft.PSharp.StaticAnalysis
109
{

‎Source/StaticAnalysis/Summarization/StateMachines/OnExitMachineAction.cs

-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@
44
// ------------------------------------------------------------------------------------------------
55

66
using Microsoft.CodeAnalysis.CSharp.Syntax;
7-
using Microsoft.PSharp.DataFlowAnalysis;
87

98
namespace Microsoft.PSharp.StaticAnalysis
109
{

‎Source/StaticAnalysis/Tracing/TraceInfo.cs

-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33
// Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
44
// ------------------------------------------------------------------------------------------------
55

6-
using System;
76
using System.Collections.Generic;
87

98
using Microsoft.CodeAnalysis;

‎Source/TestingServices/Engines/ITestingEngine.cs

-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@
44
// ------------------------------------------------------------------------------------------------
55

66
using System;
7-
using Microsoft.PSharp.IO;
87

98
namespace Microsoft.PSharp.TestingServices
109
{

‎Source/TestingServices/Events/QuiescentEvent.cs

-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33
// Licensed under the MIT License (MIT). See License.txt in the repo root for license information.
44
// ------------------------------------------------------------------------------------------------
55

6-
using System;
76
using System.Runtime.Serialization;
87

98
namespace Microsoft.PSharp

‎Source/TestingServices/Properties/InternalsVisibleTo.cs

-6
Original file line numberDiff line numberDiff line change
@@ -32,12 +32,6 @@
3232
"d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
3333
"ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
3434
"3bc97f9e")]
35-
[assembly: InternalsVisibleTo("PSharpTraceViewer,PublicKey=" +
36-
"0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
37-
"53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
38-
"d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
39-
"ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
40-
"3bc97f9e")]
4135
[assembly: InternalsVisibleTo("PSharpTestLauncher,PublicKey=" +
4236
"0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
4337
"53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +

‎Source/TestingServices/Properties/codeanalysis.ruleset

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@
1919
<Rule Id="CA1305" Action="None" />
2020
<Rule Id="CA1307" Action="None" />
2121
<Rule Id="CA1707" Action="Error" />
22-
<Rule Id="CA1710" Action="Error" />
22+
<Rule Id="CA1710" Action="None" />
2323
<Rule Id="CA1715" Action="None" />
2424
<Rule Id="CA1716" Action="None" />
2525
<Rule Id="CA1720" Action="None" />

‎Source/TestingServices/Tracing/Error/BugTrace.cs

+5-3
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ namespace Microsoft.PSharp.TestingServices.Tracing.Error
1616
/// some end state.
1717
/// </summary>
1818
[DataContract]
19-
internal sealed class BugTrace : IEnumerable, IEnumerable<BugTraceStep>
19+
public sealed class BugTrace : IEnumerable, IEnumerable<BugTraceStep>
2020
{
2121
/// <summary>
2222
/// The steps of the bug trace.
@@ -27,15 +27,15 @@ internal sealed class BugTrace : IEnumerable, IEnumerable<BugTraceStep>
2727
/// <summary>
2828
/// The number of steps in the bug trace.
2929
/// </summary>
30-
internal int Count
30+
public int Count
3131
{
3232
get { return this.Steps.Count; }
3333
}
3434

3535
/// <summary>
3636
/// Index for the bug trace.
3737
/// </summary>
38-
internal BugTraceStep this[int index]
38+
public BugTraceStep this[int index]
3939
{
4040
get { return this.Steps[index]; }
4141
set { this.Steps[index] = value; }
@@ -212,6 +212,7 @@ internal BugTraceStep Peek()
212212
/// <summary>
213213
/// Returns an enumerator.
214214
/// </summary>
215+
/// <returns>The enumerator.</returns>
215216
IEnumerator IEnumerable.GetEnumerator()
216217
{
217218
return this.Steps.GetEnumerator();
@@ -220,6 +221,7 @@ IEnumerator IEnumerable.GetEnumerator()
220221
/// <summary>
221222
/// Returns an enumerator.
222223
/// </summary>
224+
/// <returns>The enumerator.</returns>
223225
IEnumerator<BugTraceStep> IEnumerable<BugTraceStep>.GetEnumerator()
224226
{
225227
return this.Steps.GetEnumerator();

0 commit comments

Comments
 (0)