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..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,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 } 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": ""} diff --git a/psakefile.ps1 b/psakefile.ps1 new file mode 100644 index 0000000..1ca5745 --- /dev/null +++ b/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 '.' +} 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..7842a45 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 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'