From 90e5a527e91eb3dc3d43b5ceae0afe894138e99a Mon Sep 17 00:00:00 2001 From: Richard Bolhofer <20459042+SignalRichard@users.noreply.github.com> Date: Fri, 7 Nov 2025 15:51:07 -0500 Subject: [PATCH 1/6] feat: convert scripts to psake for ci --- README.md | 13 ++++++---- .../no_single_instance_characters.rego | 12 +++++---- psakefile.ps1 | 25 +++++++++++++++++++ requirements.psd1 | 5 ++++ .../NoSingleInstanceCharacters.psd1 | 2 +- .../Public/ConvertFrom-PlusCal.ps1 | 21 ++++++++++++++++ .../Public/Debug-Policy.ps1 | 19 ++++++++++++++ .../Public/Debug-Script.ps1 | 20 +++++++++++++++ .../Public/Test-Model.ps1 | 22 ++++++++++++++++ .../Public/Test-Policy.ps1 | 19 ++++++++++++++ .../Public/Test-Script.ps1 | 20 +++++++++++++++ .../Public/Test-Solution.ps1 | 19 ++++++++++++++ scripts/build.ps1 | 9 +------ scripts/run.ps1 | 1 - 14 files changed, 187 insertions(+), 20 deletions(-) create mode 100644 psakefile.ps1 create mode 100644 scripts/NoSingleInstanceCharacters/Public/ConvertFrom-PlusCal.ps1 create mode 100644 scripts/NoSingleInstanceCharacters/Public/Debug-Policy.ps1 create mode 100644 scripts/NoSingleInstanceCharacters/Public/Debug-Script.ps1 create mode 100644 scripts/NoSingleInstanceCharacters/Public/Test-Model.ps1 create mode 100644 scripts/NoSingleInstanceCharacters/Public/Test-Policy.ps1 create mode 100644 scripts/NoSingleInstanceCharacters/Public/Test-Script.ps1 create mode 100644 scripts/NoSingleInstanceCharacters/Public/Test-Solution.ps1 diff --git a/README.md b/README.md index 4381baa..c59cf44 100644 --- a/README.md +++ b/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 ""` -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,7 +103,7 @@ 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. @@ -108,7 +111,7 @@ A console application will be created under the project directory, `src/RemoveSi 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 diff --git a/policy/no_single_instance_characters/no_single_instance_characters.rego b/policy/no_single_instance_characters/no_single_instance_characters.rego index 1ef03c6..dbf8747 100644 --- a/policy/no_single_instance_characters/no_single_instance_characters.rego +++ b/policy/no_single_instance_characters/no_single_instance_characters.rego @@ -1,5 +1,7 @@ package no_single_instance_characters +default _characters := {x | x := 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 } diff --git a/psakefile.ps1 b/psakefile.ps1 new file mode 100644 index 0000000..5e22a46 --- /dev/null +++ b/psakefile.ps1 @@ -0,0 +1,25 @@ +properties { + $ApplicationFilePath = $ApplicationFilePath +} + +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-Model -SpecFilePath 'spec/RemoveSingleInstanceCharacters/RemoveSingleInstanceCharacters.tla' +} + +task Lint -depends Init { + Debug-Policy -PolicyDirectory './policy' + Debug-Script -ScriptsDirectory '.' +} diff --git a/requirements.psd1 b/requirements.psd1 index 56ca06e..d0d6b71 100644 --- a/requirements.psd1 +++ b/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' diff --git a/scripts/NoSingleInstanceCharacters/NoSingleInstanceCharacters.psd1 b/scripts/NoSingleInstanceCharacters/NoSingleInstanceCharacters.psd1 index f46eee0..258a688 100644 --- a/scripts/NoSingleInstanceCharacters/NoSingleInstanceCharacters.psd1 +++ b/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 = @() diff --git a/scripts/NoSingleInstanceCharacters/Public/ConvertFrom-PlusCal.ps1 b/scripts/NoSingleInstanceCharacters/Public/ConvertFrom-PlusCal.ps1 new file mode 100644 index 0000000..94d8545 --- /dev/null +++ b/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 diff --git a/scripts/NoSingleInstanceCharacters/Public/Debug-Policy.ps1 b/scripts/NoSingleInstanceCharacters/Public/Debug-Policy.ps1 new file mode 100644 index 0000000..fde7f1a --- /dev/null +++ b/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 diff --git a/scripts/NoSingleInstanceCharacters/Public/Debug-Script.ps1 b/scripts/NoSingleInstanceCharacters/Public/Debug-Script.ps1 new file mode 100644 index 0000000..836425f --- /dev/null +++ b/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 diff --git a/scripts/NoSingleInstanceCharacters/Public/Test-Model.ps1 b/scripts/NoSingleInstanceCharacters/Public/Test-Model.ps1 new file mode 100644 index 0000000..86422cf --- /dev/null +++ b/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 diff --git a/scripts/NoSingleInstanceCharacters/Public/Test-Policy.ps1 b/scripts/NoSingleInstanceCharacters/Public/Test-Policy.ps1 new file mode 100644 index 0000000..6bb1021 --- /dev/null +++ b/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 diff --git a/scripts/NoSingleInstanceCharacters/Public/Test-Script.ps1 b/scripts/NoSingleInstanceCharacters/Public/Test-Script.ps1 new file mode 100644 index 0000000..ef24e8d --- /dev/null +++ b/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 diff --git a/scripts/NoSingleInstanceCharacters/Public/Test-Solution.ps1 b/scripts/NoSingleInstanceCharacters/Public/Test-Solution.ps1 new file mode 100644 index 0000000..f581fbe --- /dev/null +++ b/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 diff --git a/scripts/build.ps1 b/scripts/build.ps1 index fac534d..12c467c 100644 --- a/scripts/build.ps1 +++ b/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 -TaskList @("ContinuousIntegration") diff --git a/scripts/run.ps1 b/scripts/run.ps1 index 56de19c..597fe27 100644 --- a/scripts/run.ps1 +++ b/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' From 5926fe62d2b850d2b44c91d939fda1e39111c101 Mon Sep 17 00:00:00 2001 From: Richard Bolhofer <20459042+SignalRichard@users.noreply.github.com> Date: Fri, 7 Nov 2025 15:53:34 -0500 Subject: [PATCH 2/6] build: fix default psake task --- scripts/build.ps1 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/build.ps1 b/scripts/build.ps1 index 12c467c..7842a45 100644 --- a/scripts/build.ps1 +++ b/scripts/build.ps1 @@ -1,2 +1,2 @@ ./scripts/Install-Dependencies.ps1 -Invoke-psake -TaskList @("ContinuousIntegration") +Invoke-psake From 4e0365c8c0d98b62f423a197ceaf16187cf8f665 Mon Sep 17 00:00:00 2001 From: Richard Bolhofer <20459042+SignalRichard@users.noreply.github.com> Date: Fri, 7 Nov 2025 15:54:40 -0500 Subject: [PATCH 3/6] build: remove unused parameters --- psakefile.ps1 | 4 ---- 1 file changed, 4 deletions(-) diff --git a/psakefile.ps1 b/psakefile.ps1 index 5e22a46..c82879c 100644 --- a/psakefile.ps1 +++ b/psakefile.ps1 @@ -1,7 +1,3 @@ -properties { - $ApplicationFilePath = $ApplicationFilePath -} - task default -depends Init, Build, Test, Lint task Init { From c5eedc3ec1d766e3836c8602f60ec6dedbf5f7f0 Mon Sep 17 00:00:00 2001 From: Richard Bolhofer <20459042+SignalRichard@users.noreply.github.com> Date: Fri, 7 Nov 2025 16:03:22 -0500 Subject: [PATCH 4/6] chore: regal lint --- .../no_single_instance_characters.rego | 2 +- .../no_single_instance_characters_test.rego | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/policy/no_single_instance_characters/no_single_instance_characters.rego b/policy/no_single_instance_characters/no_single_instance_characters.rego index dbf8747..a3f3a46 100644 --- a/policy/no_single_instance_characters/no_single_instance_characters.rego +++ b/policy/no_single_instance_characters/no_single_instance_characters.rego @@ -1,6 +1,6 @@ package no_single_instance_characters -default _characters := {x | x := data.characters[_]} +default _characters := {c | some c in data.characters} default valid := false diff --git a/policy/no_single_instance_characters/no_single_instance_characters_test.rego b/policy/no_single_instance_characters/no_single_instance_characters_test.rego index 4765a37..0428ed6 100644 --- a/policy/no_single_instance_characters/no_single_instance_characters_test.rego +++ b/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": ""} From 1cfdceffc7fb76e6b0944c8c3b6de0ff059bae0f Mon Sep 17 00:00:00 2001 From: Richard Bolhofer <20459042+SignalRichard@users.noreply.github.com> Date: Fri, 7 Nov 2025 16:05:27 -0500 Subject: [PATCH 5/6] build: add module imports --- psakefile.ps1 | 2 ++ 1 file changed, 2 insertions(+) diff --git a/psakefile.ps1 b/psakefile.ps1 index c82879c..17a0e4f 100644 --- a/psakefile.ps1 +++ b/psakefile.ps1 @@ -2,6 +2,8 @@ task default -depends Init, Build, Test, Lint task Init { Import-Module -Name './scripts/NoSingleInstanceCharacters' + Import-Module -Name 'Pester' + Import-Module -Name 'PSScriptAnalyzer' } task Build -depends Init { From 6595df8047095feca7ad0edcc3d47a0ac6ceaf90 Mon Sep 17 00:00:00 2001 From: Richard Bolhofer <20459042+SignalRichard@users.noreply.github.com> Date: Fri, 7 Nov 2025 16:06:54 -0500 Subject: [PATCH 6/6] build: add missing test for scripts --- psakefile.ps1 | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/psakefile.ps1 b/psakefile.ps1 index 17a0e4f..1ca5745 100644 --- a/psakefile.ps1 +++ b/psakefile.ps1 @@ -2,8 +2,6 @@ task default -depends Init, Build, Test, Lint task Init { Import-Module -Name './scripts/NoSingleInstanceCharacters' - Import-Module -Name 'Pester' - Import-Module -Name 'PSScriptAnalyzer' } task Build -depends Init { @@ -14,6 +12,7 @@ task Build -depends Init { 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' }