ci: add psake

README.md

@@ -48,6 +48,7 @@ The following optional tooling is also used:
 
 * `regal` - OPA/Rego linting
 * `Pester` - PowerShell module for unit testing
+* `Psake` - PowerShell module automation tool
 * `PSScriptAnalyzer` - PowerShell module for linting
 
 ### Quickstart
@@ -69,7 +70,9 @@ columns 6
   spec-- "implemented as" -->opa
 ```
 
-First, run `dotnet build` from the repository root to build the sample implementation.
+To run the PowerShell commands, first run `Import-Module -Name './scripts/NoSingleInstanceCharacters`
+
+To build the sample implementation, run `Build-Solution` from the repository root to build the sample implementation.
 
 If you have `opa`, and `PowerShell` installed you can run the [run.ps1](scripts/run.ps1) script from the repository root and it will run the OPA server and run the console application with a set of predefined inputs that will get validated by calling the OPA server.
 
@@ -81,7 +84,7 @@ You can also pass your own executable/application file path to the script so tha
 
 `./scripts/run.ps1 -ApplicationFilePath "<full-path-to-my-exe>"`
 
-To run the PowerShell Pester tests, run `Invoke-Pester -Path './NoSingleInstanceCharacters'` inside the `/scripts` folder.
+To run the PowerShell Pester tests, run `Test-Script` from the repository root.
 
 > If the command `Invoke-Pester` is not found, ensure you have installed the `Pester` module either directly of via the [requirements.psd1](requirements.psd1) using `PSDepend` (see [Install-Dependencies.ps1](scripts/Install-Dependencies.ps1) for PowerShell setup).
 
@@ -100,15 +103,15 @@ The following sections provide overviews of the different sections of code and h
 
 The sample implementation is written in C# and can be found in the [Extensions.cs](src/RemoveSingleInstanceCharacters/Extensions.cs) file.
 
-To build the implementation, run `dotnet build` from the repository root.
+To build the implementation, run `dotnet build` (or `Build-Solution`) from the repository root.
 
 A console application will be created under the project directory, `src/RemoveSingleInstanceCharacters/bin/Debug/net8.0/RemoveSingleInstanceCharacters.exe`.  You can run this console application with an argument and will output the result.
 
 `RemoveSingleInstanceCharacters.exe "test 123"`
 
 The single instance characters that are removed can be changed by updating the [appsettings.json](src/RemoveSingleInstanceCharacters/appsettings.json) file.
 
-To run the unit tests, run `dotnet test` in the repository root.
+To run the unit tests, run `dotnet test` (or `Test-Solution`) in the repository root.
 
 ### Validation Code
 
@@ -136,7 +139,7 @@ You can use this as a validation system for writing your own implementations of
 
 The single instance characters that are checked can be changed by updating the [data.json](policy/data.json) file.
 
-To run the policy tests, run `opa test . -v` inside the `/policy` folder.
+To run the policy tests, run `opa test . -v` inside the `/policy` folder or run `Test-Policy` from the repository root.
 
 ### Formal Methods/Specification
 

policy/no_single_instance_characters/no_single_instance_characters.rego

@@ -1,5 +1,7 @@
 package no_single_instance_characters
 
+default _characters := {c | some c in data.characters}
+
 default valid := false
 
 # METADATA
@@ -24,19 +26,19 @@ _is_valid(n, arr) if {
 	# \/ ~({ result[n] } \subseteq singleInstance)
 
 	c := arr[n]
-	count({c} & data.characters) == 0
+	count({c} & _characters) == 0
 }
 
 _is_valid(n, arr) if {
 	# \/ { result[n] } \subseteq singleInstance) /\ ((n - 1 >= 1 /\ { result[n - 1] } \subseteq singleInstance)
 	n - 1 >= 0
-	count({arr[n]} & data.characters) > 0
-	count({arr[n - 1]} & data.characters) > 0
+	count({arr[n]} & _characters) > 0
+	count({arr[n - 1]} & _characters) > 0
 }
 
 _is_valid(n, arr) if {
 	# \/ (n + 1 <= Len(result) /\ { result[n + 1] } \subseteq singleInstance)
 	n + 1 < count(arr)
-	count({arr[n]} & data.characters) > 0
-	count({arr[n + 1]} & data.characters) > 0
+	count({arr[n]} & _characters) > 0
+	count({arr[n + 1]} & _characters) > 0
 }

policy/no_single_instance_characters/no_single_instance_characters_test.rego

@@ -2,7 +2,7 @@ package no_single_instance_characters_test
 
 import data.no_single_instance_characters
 
-characters := {"0", "2", "4", "6", "8"}
+characters := ["0", "2", "4", "6", "8"]
 
 test_valid_when_empty if {
 	no_single_instance_characters.valid with input as {"str": ""}

psakefile.ps1

@@ -0,0 +1,22 @@
+task default -depends Init, Build, Test, Lint
+
+task Init {
+    Import-Module -Name './scripts/NoSingleInstanceCharacters'
+}
+
+task Build -depends Init {
+    Build-Solution -SolutionFilePath './RemoveSingleInstanceCharacters.sln'
+    ConvertFrom-PlusCal -SpecFilePath 'spec/RemoveSingleInstanceCharacters/RemoveSingleInstanceCharacters.tla'
+}
+
+task Test -depends Build, Init {
+    Test-Solution -SolutionFilePath './RemoveSingleInstanceCharacters.sln'
+    Test-Policy -PolicyDirectory './policy'
+    Test-Script -ScriptsDirectory './scripts'
+    Test-Model -SpecFilePath 'spec/RemoveSingleInstanceCharacters/RemoveSingleInstanceCharacters.tla'
+}
+
+task Lint -depends Init {
+    Debug-Policy -PolicyDirectory './policy'
+    Debug-Script -ScriptsDirectory '.'
+}

requirements.psd1

@@ -8,6 +8,11 @@
         DependencyType = 'PSGalleryModule'
         Version = '5.7.1'
     }
+    Psake = @{
+        Name = 'psake'
+        DependencyType = 'PSGalleryModule'
+        Version = '4.9.1'
+    }
     PSScriptAnalyzer = @{
         Name = 'PSScriptAnalyzer'
         DependencyType = 'PSGalleryModule'

scripts/NoSingleInstanceCharacters/NoSingleInstanceCharacters.psd1

@@ -65,7 +65,7 @@ PowerShellVersion = '7.4'
 # NestedModules = @()
 
 # Functions to export from this module, for best performance, do not use wildcards and do not delete the entry, use an empty array if there are no functions to export.
-FunctionsToExport = @('Build-Solution', 'Import-Test', 'Invoke-Application', 'Invoke-OpenPolicyAgent', 'Start-OpenPolicyAgent', 'Test-Application')
+FunctionsToExport = @('Build-Solution', 'ConvertFrom-PlusCal', 'Debug-Policy', 'Debug-Script', 'Import-Test', 'Invoke-Application', 'Invoke-OpenPolicyAgent', 'Start-OpenPolicyAgent', 'Test-Application', 'Test-Model', 'Test-Policy', 'Test-Script', 'Test-Solution')
 
 # Cmdlets to export from this module, for best performance, do not use wildcards and do not delete the entry, use an empty array if there are no cmdlets to export.
 CmdletsToExport = @()

scripts/NoSingleInstanceCharacters/Public/ConvertFrom-PlusCal.ps1

@@ -0,0 +1,21 @@
+<#
+.Synopsis
+    Runs PlusCal to TLA+ conversion.
+.DESCRIPTION
+    Runs PlusCal to TLA+ conversion.
+.EXAMPLE
+    ConvertFrom-PlusCal -SpecFilePath './spec/RemoveSingleInstanceCharacters/RemoveSingleInstanceCharacters.ps1'
+.INPUTS
+    System.String. The spec file path.
+#>
+
+function ConvertFrom-PlusCal {
+    param(
+        [string] $SpecFilePath,
+        [string] $TLA2ToolsFilePath = '/usr/local/bin/tla2tools.jar'
+    )
+
+    java -cp $TLA2ToolsFilePath pcal.trans $SpecFilePath
+}
+
+Export-ModuleMember -Function ConvertFrom-PlusCal

scripts/NoSingleInstanceCharacters/Public/Debug-Policy.ps1

@@ -0,0 +1,19 @@
+<#
+.Synopsis
+    Lints the policies.
+.DESCRIPTION
+    Lints the policies.
+.EXAMPLE
+    Debug-Policy -PolicyDirectory './policy'
+.INPUTS
+    System.String. The policy directory.
+#>
+
+function Debug-Policy {
+    param(
+        [string] $PolicyDirectory
+    )
+    regal lint $PolicyDirectory
+}
+
+Export-ModuleMember -Function Debug-Policy

scripts/NoSingleInstanceCharacters/Public/Debug-Script.ps1

@@ -0,0 +1,20 @@
+<#
+.Synopsis
+    Lints PowerShell.
+.DESCRIPTION
+    Lints PowerShell.
+.EXAMPLE
+    Debug-Script -ScriptsDirectory './scripts'
+.INPUTS
+    System.String. The scripts directory.
+#>
+
+function Debug-Script {
+    param(
+        [string] $ScriptsDirectory
+    )
+
+    Invoke-ScriptAnalyzer -Path $ScriptsDirectory -Recurse
+}
+
+Export-ModuleMember -Function Debug-Script

scripts/NoSingleInstanceCharacters/Public/Test-Model.ps1

@@ -0,0 +1,22 @@
+<#
+.Synopsis
+    Runs the TLC model checker.
+.DESCRIPTION
+    Runs the TLC model checker.
+.EXAMPLE
+    Test-Model -SpecFilePath './spec/RemoveSingleInstanceCharacters/RemoveSingleInstanceCharacters.ps1'
+.INPUTS
+    System.String. The spec file path.
+#>
+
+function Test-Model {
+    param(
+        [string] $SpecFilePath,
+        [string] $TLA2ToolsFilePath = '/usr/local/bin/tla2tools.jar',
+        [string] $Options = '-deadlock'
+    )
+
+    java -XX:+IgnoreUnrecognizedVMOptions -XX:+UseParallelGC -cp $TLA2ToolsFilePath tlc2.TLC $Options $SpecFilePath
+}
+
+Export-ModuleMember -Function Test-Model

scripts/NoSingleInstanceCharacters/Public/Test-Policy.ps1

@@ -0,0 +1,19 @@
+<#
+.Synopsis
+    Tests the policies.
+.DESCRIPTION
+    Tests the policies.
+.EXAMPLE
+    Test-Policy -PolicyDirectory './policy'
+.INPUTS
+    System.String. The policy directory.
+#>
+
+function Test-Policy {
+    param(
+        [string] $PolicyDirectory
+    )
+    opa test $PolicyDirectory
+}
+
+Export-ModuleMember -Function Test-Policy

scripts/NoSingleInstanceCharacters/Public/Test-Script.ps1

@@ -0,0 +1,20 @@
+<#
+.Synopsis
+    Pester PowerShell.
+.DESCRIPTION
+    Pester PowerShell.
+.EXAMPLE
+    Test-Script -ScriptsDirectory './scripts'
+.INPUTS
+    System.String. The scripts directory.
+#>
+
+function Test-Script {
+    param(
+        [string] $ScriptsDirectory
+    )
+
+    Invoke-Pester -Path $ScriptsDirectory
+}
+
+Export-ModuleMember -Function Test-Script

scripts/NoSingleInstanceCharacters/Public/Test-Solution.ps1

@@ -0,0 +1,19 @@
+<#
+.Synopsis
+    Tests the provided dotnet solution file.
+.DESCRIPTION
+    Tests the provided dotnet solution file.
+.EXAMPLE
+    Build-Solution -SolutionFilePath './solution.sln'
+.INPUTS
+    System.String. The solution file path.
+#>
+
+function Test-Solution {
+    param(
+        [string] $SolutionFilePath
+    )
+    dotnet test $SolutionFilePath
+}
+
+Export-ModuleMember -Function Test-Solution

scripts/build.ps1

@@ -1,9 +1,2 @@
 ./scripts/Install-Dependencies.ps1
-
-dotnet build
-dotnet test
-opa test ./policy
-Invoke-Pester -Path ./scripts/NoSingleInstanceCharacters
-Invoke-ScriptAnalyzer -Path scripts -Recurse
-java -cp "/usr/local/bin/tla2tools.jar" pcal.trans "spec/RemoveSingleInstanceCharacters/RemoveSingleInstanceCharacters.tla"
-java -XX:+IgnoreUnrecognizedVMOptions -XX:+UseParallelGC -cp "/usr/local/bin/tla2tools.jar" tlc2.TLC "-deadlock" "spec/RemoveSingleInstanceCharacters/RemoveSingleInstanceCharacters.tla"
+Invoke-psake

scripts/run.ps1

@@ -10,4 +10,3 @@ Import-Module -Name (Join-Path -Path $PSScriptRoot -ChildPath 'NoSingleInstanceC
 $opaProcess = Start-OpenPolicyAgent -PolicyDirectoryPath (Join-Path -Path $PSScriptRoot -ChildPath '../policy/no_single_instance_characters')
 (Import-Test -TestsFilePath (Join-Path -Path $PSScriptRoot -ChildPath 'test_arguments.json')).tests | Test-Application -ApplicationFilePath $ApplicationFilePath
 $opaProcess | Stop-Process
-Remove-Module -Name 'NoSingleInstanceCharacters'