Added PSharp as a submodule

p-org · Mar 24, 2017 · 434dcac · 434dcac
1 parent e879699
commit 434dcac
Show file tree

Hide file tree

Showing 5 changed files with 27 additions and 6 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -5,3 +5,6 @@
 [submodule "Ext/Formula"]
 	path = Ext/Formula
 	url = https://github.com/Microsoft/formula.git
+[submodule "Ext/PSharp"]
+	path = Ext/PSharp
+	url = https://github.com/p-org/PSharp.git
diff --git a/Bld/build.bat b/Bld/build.bat
@@ -117,6 +117,15 @@ for %%i in (zc\bin\%Platform%\Release\zc.exe
 
 cd ..\..
 
+REM Build PSharp
+cd ext\PSharp
+..\..\Bld\nuget restore PSharp.sln
+echo devenv PSharp.sln /Build %Configuration%
+devenv PSharp.sln /Build %Configuration%
+if ERRORLEVEL 1 goto :exit
+
+cd ..\..
+
 if "%NoClean%"=="true" goto :build
 echo msbuild P.sln /p:Platform=%Platform% /p:Configuration=%Configuration%  /t:Clean
 msbuild  P.sln /p:Platform=%Platform% /p:Configuration=%Configuration% /t:Clean
@@ -161,4 +170,4 @@ echo Elapsed: %TookTime:~0,-2%.%TookTimePadded:~-2% seconds
 goto :EOF
 
 :exit
-popd
+popd
diff --git a/Ext/PSharp b/Ext/PSharp
diff --git a/Src/PTester/PTester/PTester.csproj b/Src/PTester/PTester/PTester.csproj
@@ -141,11 +141,13 @@
     <Prefer32Bit>false</Prefer32Bit>
   </PropertyGroup>
   <ItemGroup>
-    <Reference Include="Microsoft.PSharp">
-      <HintPath>..\..\..\..\PSharp\Binaries\Microsoft.PSharp.dll</HintPath>
+    <Reference Include="Microsoft.PSharp, Version=1.1.0.0, Culture=neutral, PublicKeyToken=c4566cf0a7f74012, processorArchitecture=MSIL">
+      <SpecificVersion>False</SpecificVersion>
+      <HintPath>..\..\..\Ext\PSharp\Binaries\Microsoft.PSharp.dll</HintPath>
     </Reference>
-    <Reference Include="Microsoft.PSharp.TestingServices">
-      <HintPath>..\..\..\..\PSharp\Binaries\Microsoft.PSharp.TestingServices.dll</HintPath>
+    <Reference Include="Microsoft.PSharp.TestingServices, Version=1.1.0.0, Culture=neutral, PublicKeyToken=c4566cf0a7f74012, processorArchitecture=MSIL">
+      <SpecificVersion>False</SpecificVersion>
+      <HintPath>..\..\..\Ext\PSharp\Binaries\Microsoft.PSharp.TestingServices.dll</HintPath>
     </Reference>
     <Reference Include="System">
       <Name>System</Name>

diff --git a/Src/PTester/PTester/PTesterCommandLine.cs b/Src/PTester/PTester/PTesterCommandLine.cs
@@ -198,6 +198,12 @@ public static void Main(string[] args)
                 Environment.Exit((int)TestResult.InvalidParameters);
             }
 
+            if (options.UsePSharp && options.isRefinement)
+            {
+                Console.WriteLine("Error: Refinement checking isn't yet supported with /psharp flag");
+                Environment.Exit((int)TestResult.InvalidParameters);
+            }
+
             if (options.isRefinement)
             {
                 var refinementCheck = new RefinementChecking(options);
@@ -294,7 +300,7 @@ public static void RunPSharpTester(StateImpl s)
             configuration.MaxUnfairSchedulingSteps = 100;
             configuration.MaxFairSchedulingSteps = configuration.MaxUnfairSchedulingSteps * 10;
             configuration.LivenessTemperatureThreshold = configuration.MaxFairSchedulingSteps / 3;
-
+            
             var engine = Microsoft.PSharp.TestingServices.TestingEngineFactory.CreateBugFindingEngine(
                 configuration, PSharpWrapper.Execute);
             engine.Run();