Skip to content

Commit 5367942

Browse files
ankushdesaiaman-goelehua9146Eric Huamchadalavada
authored
Merging PEx into the Major release P 3.0 branch. (#860)
* Removed the C backend completely in the P 2.1 * Upgraded P to use .Net 8.0 * Updated the actions to .Net 8.0 * [PSym] Upgrade to .NET 8.0 * [PCover] Adds temporary CLI mode to trigger new explicit engine * [PCover] Adds initial version of cleaned up PCover backend TODO: Implement basic new runtime interface to pass code compilation post generation * [PCover] Minor * [PCover IR] Cleans up logic relating to event handlers Removes using PMachineValue for now * [CLI] Adds new pcover cli (hidden) * [PCover IR] Cleanup IR for sending event, machine creation, etc. * [PCover runtime] Adds basic runtime setup files * [PCover] Adds placeholder for CLI config * [PCover] Adds main and trace loggers using Log4J * [PCover] Adds event buffer represented as fifo queue with sender semantics * [PCover] Adds event handler placeholders * [PCover] Adds event/message placeholders * [PCover] Adds basic code for machine/state/test driver * [PCover] Adds basic code for scheduler * [PCover] Adds global data structures and program interface * [PCover] Adds utils * [PCover IR] Minor renaming * [PCover] Adds PValues for P data types * [PCover] Renaming and minor corrections Renames Machine/Monitor/Program to PMachine/PMonitor/PModel Corrects PBool value * [PCover] Minor update to javadocs * [PCover] Reformating * [PCover IR+RT] Rename Message to PMessage * [CLI] Minor correction * [PExplicit] Renames new PCover to PExplicit * [PExplicit] Minor correction to CLI * [PExplicit RT] Rename repeat to current, backtrack to unexplored choices * [PExplicit RT] Adds CLI options and config * [PExplicit RT] Adds new exceptions when a bug is found * [PExplicit RT] Adds timeout/memout monitors * [Pexplicit RT] Adds utils for timed call, random number generator, and in-line asserts * [Pexplicit RT] Adds more logging functions * [PExplicit RT] Updates machine and message queues to check if machine can run and if a message is a create machine event * [PExplicit RT] Add function to check if an event is a create machine event * [PExplicit RT] Improve choices and schedule fields * [PExplicit RT] Implements main PExplicit fentry point, runtime executor service, making timed call Deletes DeferQueue. Instead the plan is to handle defers as in C# runtime. Updates global fields * [PExplicit RT] Updates loggers Adds new log functions to the main logger, adds a scratch logger for intermediate printing * [PExplicit RT] Implements and cleans up certain PMachine/State functions * [PExplicit RT] Adds initial version of scheduler Work in progress: finish pending TODOs and JavaDoc comments * [PExplicit RT] Implements basic machine/scheduler/FIFO functions TODOs: receives, defers, etc. * [PExplicit RT] Adds initial support for stateless dfs-style backtracking Adds tracking all machine instances in global context * [PExplicit IR] Removes StringVS TODO: support formatted arguments in PString in RT * [PExplicit RT] Corrects basic dfs-search Corrects adding new machines to global and schedule context Adds basic functions for PMessage Corrects scheduler DFS-style search working on pingPong * [PExplicit RT] Improves how peeking into a machine's FIFO queue works * [PExplicit] Support formatted PString, initial support for defers and receives Adds support for formatted string Adds continuations to runtime and cleans up IR with a simplified interface Adds partial support for defers and receives TODO: finish defer and receive handling * [PExplicit RT] Adds support for defers and blocking receive Adds tracking deferred events via a defer queue Adds PContinuation to track all continuations Adds blocking on a continuation, and unblocking when handling one of the corresponding case event Corrects peeking logic in sender queue Renames FifoQueue to SenderQueue * [PExplicit] Adds support for receives, loops, and named tuple constructor Cleans up support for receives. Adds support for receives within while loop Simplifies IR for loops Updates PValue for PCollection types Corrects constructor for PNamedTuple * [PExplicit] Implements operations for primitive PValue types Minor renaming * [PExplicit] Adds running mvn test and github ci action * [PExplicit RT] Implement raising an event * Disable GitHub CI actions temporarily to only run PExplicit CI * [PExplicit] Several minor updates Support goto event handlers with transition functions Correct PTuple constructor Correct status and result when a bug is bound Cleanup return in functions in IR. Start adding pending/unsupported tests in PExplicit test runner * [PExplicit] Support announce, correct named tuple set ffield, support != operation * [PExplicit] Several corrections Implement raise event, updates logging, updates PCollection to be an interface, updates exclude list for regression runs Adds enforcing max step bound * [PExplicit] Correct raise event with payload * [PExplicit] Correct PString constructor * [PExplicit IR] Exit current flow context if raise or goto statements are present * Update gitignore * [PExplicit] Several corrections Changes PCollection types to not take parameters (so that collections over any type can be allowed) Corrects choosing from a PCollection Corrects IR to track whether function exited or not Avoid printing redundant code if receive cases already exited * [PExplicit] Support enum references with values specified Support enum to int Update excluded regressions list * [PExplicit IR] Correct dynamic type casting in IR * Suppress github ci failures due to not running them on current branch * [PExplicit] Cleaned up type casting in IR Added type casting regressions Corrected PTuple set field * [PExplicit] Support continue statement Remove unreachable code after receive case block * [PExplicit] Several small upgrades Support blocking receives during state transitions and exit functions Support getting values of a PMap Add logging for entering and exiting a state * [PExplicit] Several corrections and minor lang feature support Corrects type casting from any when a function returns a value Adds catching null pointer and stack overflow exceptions as a bug Implement get or default from a PMap Comments out liveness test regressions for now (added TODO) Cleans up PMachineValue constructor * [PExplicit] Refactoring and cleanup * Undo temporary changes to GitHub CI * [PExplicit] Update pom, minor refactoring * [PExplicit] Update to java 17 * [PExplicit] Minor: report class cast exception as a bug * [PExplicit] Convert run status to enum * [PExplicit] Clean up control flow relating to pending state transition (exit/new-state-entry) Renames blockedEntryState to blockedNewStateEntry * [PExplicit] Update comments * Added support for generating a warning when spec handles an event but does not add it in its observes list (#716) * Create custom converter for JSON serialization in .NET8 (#717) * Create custom converter for JSON serialization in .NET8 * Add check for different dictionary type for null replacement --------- Co-authored-by: Eric Hua <[email protected]> * [PExplicit] Support deadlock and liveness checking Adds deadlock checking Adds basic liveness checking, based on whether a monitor is in a hot state at the end of a schedule Updates logger to resemble like in C# * [PExplicit] Minor * [PExplicit] Adds buggy trace replayer and basic .schedule writer * [PExplicit] Correct issues when replaying buggy trace Corrected catching null/class-cast errors when replaying Corrected how a machine resets (to reset variables relating to blocking receives) Corrected how current choice is fetched when replaying * [PExplicit] Adds TextWriter to write trace in txt format Updates logging * [PExplicit] Correct halt event name * [PExplicit] Adds state caching Adds state caching to avoid revisiting same state more than once State caching mode can be: none, fingerprint (i.e., use hash codes), or exact (use exact values). Fingerprinting is the default. Updates logging and stats to track and report distinct states Minor cleanup to IR * [PExplicit] Minor refactoring * [PExplicit] Correct cycle error in replayer, enforce cycle detection only when --fail-on-maxsteps enabled * [PExplicit] Correct local var names in IR * [PExplicit] Correct replayer, add initial version of stateful backtracking * [PExplicit] Correct backtracking * [PExplicit] Refactor and enable stateful backtracking * [PExplicit] Minor improvement to stateful backtracking * [PExplicit] Reformat code * [PExplicit] More reformatting * [PExplicit] Minor corrections Correct comparing machines (including monitors) Correct printing step state * [PExplicit] Correct PMachine/PMonitor hashCode and compateTo functions * [PExplicit] Uniquify instanceId for PMachine as well as PMonitor * [PExplicit] Improve state caching Adds storing hashcode and string representation during PValue initialization Adds new state caching modes using hash functions from guava library New state caching modes include: hashcode (java built in, 32-bit), siphash24 (64-bit), murmur3_128 (128-bit, default), sha256 (256-bit), or exact (using exact string representation) * [PExplicit] Add non-chronological search Adds non-chronological search that implements search beyond DFS. New search modes include random, astar Each run is executed over search tasks, with each task tracking the set of unexplored choices it is assigned to explore Each search task can create new children sub-tasks * [Pexplicit] Minor * [PExplicit] Minor refactoring * [PExplicit] Refactoring and cleanup * Limit number of choices in choose expression to at most 10000 (#725) * Limit number of choices in a choose(.) to atmost 10,000 Adds throwing a compile-time or runtime error if the number of choices in a choose(.) is greater than 10000. Updates GitHub docs to reflect this change. * Adds regression tests for choose exceeding 10000 choices * [PSym] Throw error if number of choices are greater than 10000 * Make PEvents and PTypes serializable in java (#726) * [PExplicit IR] Minor correction * [PExplicit] Update usage via P CLI * [PExplicit] Several corrections to choice tracking Change choice in a schedule to be either ScheduleChoice or DataChoice Step state does not track step/choice number, only tracks current machines and machine states (in stateful backtracking) Correct SearchTask to store full list of prefix/suffix choices. Suffix choices contain list of unexplored choices assigned to this task. Update how liveness/deadlock checking is asserted and replayed. * [PExplicit] Minor refactoring * [PExplicit] Refactoring and setting defaults * [PExplicit] Correct counting unexplored choices * [PExplicit] Minor changes to logging and asserts * [PExplicit] Throw error if number of choices in choose(.) exceeds 10K * [PExplicit] Correct stateful backtracking with complex data choices * [PEx] Minor update * [PEx] Support Java foreign functions * [PEx] Minor corrections to IR * [PEx] Minor: correct an assertion * [PEx] Make receive inside while as not implemented for now Update enum logging and stats reporting PMap: throw error if adding already existing key * [PEx] Experimenting with while and receive in IR * [PEx] Correct corner cases with while, receive, and after statements * [Tst] Add unit test to check interaction between while, receive w/ case payload, and after statements after receive and while * Removed the C backend completely in the P 2.1 * [PCover] Adds temporary CLI mode to trigger new explicit engine * [CLI] Adds new pcover cli (hidden) * [PExplicit] Renames new PCover to PExplicit * Correct sync with mainline * [PEx] Revamps tracking unexplored choices, changes schedule choice (#745) * [PEx] Change schedule choice from PMachine to PMachineId * [PEx] Major revamping of Choice: 1/n Old schedule/data choice changed to schedule/data SearchUnit Added new class for schedule/data Choice, which is just a wrapper around PMachineId/PValue<?> TODO: clean up Schedule with new class structure * Revert "[PEx] Major revamping of Choice: 1/n" This reverts commit 53c5d15. * [PEx] Separates unexplored choices from schedule * [PEx] Cleanup and minor corrections to recent changes to SearchTask * [PEx] Minor correction * [PEx] Corrections to new backtracking logic * [PEx] Adds modes for stateful backtracking Adds CLI option --stateful-backtrack none|intra-task|all to limit stateful backtracking to OFF|within-a-task|ON * [PEx] Add support to serialize and deserialize search tasks in/from file * [PEx] Updates mvn test config * [PEx] Minor correction Fix issue relating to intra-task stateful backtracking with dynamic machine creation * [PEx IR] Minor correction * [PEx] Several improvements to IR Revamps IR to store continuation variables within PContinuation class Adds function to get the default value from a PValue object Removes generating get/set/reset functions for PMachine variables. Instead, using reflection in PEx RT. Minor refactoring * [PEx IR] Minor cleanup * [PEx] Cleanup disk tasks on exit, change defaults Cleanup tasks/ directory on exiting Change default for schedules-per-task to 500 Change report wait time to 10 sec. * [PEx] Minor: create .schedule only if bug is found * [PEx] Adds writing buggy trace in file Adds serializing buggy trace in file Minor renaming * [PEx] Adds option --replay <.schedule file> to replay a buggy trace * [PEx] Minor * [PEx] Fix serialization issues found by P regression tests * [PEx] Minor cleanup * [PEx] Improve cleanup of disk tasks on exit * [PEx] Minor correction Update liveness check, minor renaming * [PEx] Add first version of RL-based choice selection * [PEx] Correct timelines tracking and RL-based choice selection * [PEx] Update timelines, corrects CI * [PEx] Renaming and refactoring Renames PExplicit -> PEx, GlobalFunctions -> PExForeignCode, mode explicit -> pex Refactors PEx IR generator * [CLI] Update PEx CLI options Makes --mode option visible. * [CLI] Cleanup PEx CLI options * [CI] Correct PEx CI * [PEx] Add support for refinement interfaces * [Tutorial] Adds updates for running with PEx Adds changes/hints to enable running with PEx 1_ClientServer: limits number of withdraw requests to at most 5, adds 2 hints to limit data non-determinism 2_TwoPhaseCommit: adds hint to create random transaction without foreign code and with less data non-determinism 3_EspressoMachine: no change * [PEx] Minor: update pom.xml * [PEx] Implements multi-threaded PEx version (#768) * [PEx] Move globals to PExGlobal, adds --nproc CLI option Moves state cache, timelines, num tasks data structures to PEx global class Adds CLI option --nproc to provide number of threads * [PEx] Adds dedicated logger for each thread Moves global results reporting to global class * [PEx] parallel: adds todos, cleans up global class * [PEx] parallel: fix IR, move scheduler specific fields from globals * [PEx] parallel: update IR so that main machine and monitors are created by PEx runtime * [PEx] parallel: make search statistics thread safe * [PEx] parallel: completes first version Several updates: support multi-thread executor, result tracking, exceptions tracking, compiling results, terminating threads, resolving data conflicts, implements lock/release for shared constructs * [PEx] parallel: minor change * [PEx] parallel: update GitHub CI to run with 3 threads * [PEx] parallel: minor corrections Make global machine/monitor instance ids thread safe Add hash/name to PContinuation object for thread-safe state caching * [PEx] Adds tracking and limiting number of choices per choose(.) statement Adds tracking number of calls and total choices generated in a schedule corresponding to each choose(.) statement in the model. Adds option --max-choices-per-call and --max-choices-total to limit max number of choices in a schedule corresponding to a choose(.) statement (default is 10,000 for per choose.) call and no limit on total choices, as in C# backend). Else, a TooManyChoicesException is triggered as a bug. * [PEx] bump version, change cli defaults Change max choices per choose statement to 10 per call and 100 per schedule by default Minor renaming * [PEx] code cleanup and refactoring * [PEx] minor logging changes, [Tst] Change choose(100) to choose(10) * [PEx] Minor logging changes * [PEx] Changes return codes 0: ok, 2: bug, 3: bug (too_many_choices), 4: timeout, 5: memout, 6: error * [PEx] Correct return codes, [Tst] Limit choose choices * [Tutorial] Update hints for PEx [PEx] minor change * [PEx] Minor updates and cleanup (#775) * [PEx] Several updates to logging, PEx config Changes default max choices limit to 20 per call and 250 per schedule (to account for open-source protocols with monolithic transition relation modeled as single action) Adds logging support to print choose(.) location info for easy debugging TooManyChoicesException via replayer log Minor correction * [PEx] Refactoring and formatting changes * [PEx] Update cli default Change each task to 2K schedules by default * [PEx] Minor correction Make sure continuation with loop does not declare local var twice * [PEx] Correct repeated local var declaration in IR * [PEx] Correct code too large error due to receive-inside-loop inlining * [PEx] Adds PLoopObject to track receive-loop variables * [PEx] Minor: correct defaults in help menu * modified cache@v2 to cache@v4 * Rename PEvent to Event, Handle PrimitiveType.Null in GetDefaultValue * [PEx] Correct functions containing non-tail ending goto/raise (#835) * [PEx] Correct inlining for functions returning a value (#840) * [PEx] Correct functions containing goto/raise Changes PEx IR to support functions that contain non-tail ending goto/raise Enables supporting needed function inlining in spec machines Bumps PEx runtime revision to 0.3.0 * [PEx] Remove wrongly-added files * [PEx IR] Correct function inlining for non-null returning functions Add guard conditions to disable function body statement if already returned Throw exception if inlining is unsupported * removed CSharp, Java modes in CompilerOutput , removed global.json * Minor changes to make customer model to compile (#842) * [PEx] Disable support for receive statement inside loop (#843) Throw compile-time exception for receive statement inside loop with appropriate message Adds try/catch to gracefully report not-supported errors during compiling for PEx PEX RT: exclude tests with receive inside loop * Dev/remove libhandler (#847) * Update build system and Java compiler, remove dependency JARs (#849) * Update build system and Java compiler, remove dependency JARs * Update CheckerCore logging and state machine components * [PEx] Correct inlining functions with non-null return without assignment (#850) * [PEx] Correct inlining functions with non-null return without assignment, support test driver name same as test machine name [PEx IR] Adds support for inlining functions that return non-null but are not assigned to a variable during function call [PEx IR+RT] Prefixes test driver names with test_ to support test name same as test main machine name [Tst] Adds unit test with test case name same as main machine name * [PEx IR] Correct IR for functions returning null * [Tst] Update new unit test to align with hardcoded test name in C# unit test runner * [Tst] Dropping unit test since C# test runner uses hardcoded test name and main machine * [PEx IR] Minor correction when pritning source location in exception * Moved PEx outside the PRuntimes * Update pex.yml * Update build scripts and test executor; add build documentation * Fix Java version to 17 and correct P build directory path * Pex param test (#855) * Add global constant varaibles; TODO backend * Updated BuildGlobalScope * add global variable * fix global variable types * Allow multiple tests * Add int list literal syntax * add parametric test * Quick-fix * fix bad quick-fix * add rich syntax * Small merge error * Param (#833) * update assumption * fix: add deps back * refactor: constant -> param * fix * clean the code * unify normal/param/assume tests * clean the code * rename * merging safety test parser rules * clean the code * Update github CI action v2 to v3 * iUpdate github CI action v2 to v3 on ubuntu * rename variable "param" into "parameter" to avoid keyword conflicts * T-wise combinatorial test (#837) * add twise * clean the code * Solved Concerns from Lewis: + new allow twise number be 1 + unify twise number valid condition + add unit test * add new test case * unit test for ParamAssignment.IterateAssignments * merge * fix duplicate declears bug --------- Co-authored-by: Ankush Desai <[email protected]> * PR #860 Fixes: Removed Coverage and Verification modes, fixed code quality issues, added comments for placeholders, and added missing newlines at the end of files --------- Co-authored-by: Aman Goel <[email protected]> Co-authored-by: Eric Hua <[email protected]> Co-authored-by: Eric Hua <[email protected]> Co-authored-by: mchadalavada <[email protected]> Co-authored-by: Aishwarya Jagarapu <[email protected]> Co-authored-by: aishu-j <[email protected]> Co-authored-by: ChristineZh0u <[email protected]> Co-authored-by: Zhe Zhou <[email protected]>
1 parent 8b969c9 commit 5367942

File tree

188 files changed

+15430
-115
lines changed

Some content is hidden

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

188 files changed

+15430
-115
lines changed

‎.github/workflows/pex.yml

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
# This workflow will build and test PEx, and cache/restore any dependencies to improve the workflow execution time
2+
# For more information see: https://help.github.com/actions/language-and-framework-guides/building-and-testing-java-with-maven
3+
4+
name: PEx on Ubuntu
5+
6+
on:
7+
push:
8+
pull_request:
9+
workflow_dispatch:
10+
inputs:
11+
args:
12+
description: Additional arguments
13+
default: ""
14+
required: false
15+
jobs:
16+
PEx-Build-And-Test-Ubuntu:
17+
runs-on: ubuntu-latest
18+
steps:
19+
- uses: actions/checkout@v1
20+
- name: Setup .NET Core
21+
uses: actions/setup-dotnet@v1
22+
with:
23+
dotnet-version: 8.0.x
24+
- name: Set up JDK
25+
uses: actions/setup-java@v1
26+
with:
27+
java-version: 17
28+
- name: Cache Maven packages
29+
uses: actions/cache@v4
30+
with:
31+
path: ~/.m2
32+
key: ${{ runner.os }}-m2-${{ hashFiles('**/pom.xml') }}
33+
restore-keys: ${{ runner.os }}-m2
34+
- name: Build PEx
35+
working-directory: Src/PEx
36+
run: ./scripts/build_and_test.sh --build
37+
- name: Test PEx
38+
working-directory: Src/PEx
39+
run: ./scripts/build_and_test.sh --test

‎.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -230,6 +230,7 @@ Bld/*
230230
!Bld/Jars/
231231
!Bld/Deps/
232232
PGenerated/
233+
PCheckerOutput/
233234
!Src/**/Zing/*.zing
234235
stubs.c
235236
*.idb

‎.gitmodules

Lines changed: 0 additions & 3 deletions
This file was deleted.

‎Ext/libhandler

Lines changed: 0 additions & 1 deletion
This file was deleted.

‎Src/PChecker/CheckerCore/Checker.cs

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -35,8 +35,7 @@ public static void Run(CheckerConfiguration configuration)
3535
Error.Write(logger, ConsoleColor.Yellow, engine.GetReport());
3636
}
3737
break;
38-
case CheckerMode.Verification:
39-
case CheckerMode.Coverage:
38+
case CheckerMode.PEx:
4039
ExhaustiveEngine.Create(configuration).Run();
4140
break;
4241
default:
@@ -54,8 +53,7 @@ public static void Run(CheckerConfiguration configuration)
5453
case CheckerMode.BugFinding:
5554
TestingProcess.Create(configuration).Run();
5655
break;
57-
case CheckerMode.Verification:
58-
case CheckerMode.Coverage:
56+
case CheckerMode.PEx:
5957
ExhaustiveEngine.Create(configuration).Run();
6058
break;
6159
default:
@@ -66,4 +64,4 @@ public static void Run(CheckerConfiguration configuration)
6664
logger.WriteLine(". Done");
6765
}
6866
}
69-
}
67+
}

‎Src/PChecker/CheckerCore/CheckerConfiguration.cs

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -238,6 +238,12 @@ public int MaxSchedulingSteps
238238
[DataMember]
239239
public string CustomStateMachineRuntimeLogType;
240240

241+
/// <summary>
242+
/// Enables debugging.
243+
/// </summary>
244+
[DataMember]
245+
public bool EnableDebugging;
246+
241247

242248
/// <summary>
243249
/// The testing scheduler unique endpoint.
@@ -269,10 +275,10 @@ public int MaxSchedulingSteps
269275
public bool DisableEnvironmentExit;
270276

271277
/// <summary>
272-
/// Additional arguments to pass to PSym.
278+
/// Additional arguments to pass to checker.
273279
/// </summary>
274280
[DataMember]
275-
public string PSymArgs;
281+
public string CheckerArgs;
276282

277283
/// <summary>
278284
/// Additional arguments to pass to JVM-based checker.
@@ -321,11 +327,12 @@ protected CheckerConfiguration()
321327
DebugActivityCoverage = false;
322328

323329
IsVerbose = false;
330+
EnableDebugging = false;
324331

325332
EnableColoredConsoleOutput = false;
326333
DisableEnvironmentExit = true;
327334

328-
PSymArgs = "";
335+
CheckerArgs = "";
329336
JvmArgs = "";
330337
}
331338

‎Src/PChecker/CheckerCore/CheckerCore.csproj

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
<AssemblyName>PCheckerCore</AssemblyName>
55
<RootNamespace>PChecker</RootNamespace>
66
<GenerateDocumentationFile>true</GenerateDocumentationFile>
7+
<NoWarn>$(NoWarn);1591</NoWarn>
78
<OutputPath>$(PSdkFolder)\Binaries</OutputPath>
89
<TargetFramework>net8.0</TargetFramework>
910
<PackageLicenseExpression>MIT</PackageLicenseExpression>
@@ -22,4 +23,4 @@
2223
<None Include="../../../Icon/icon.png" Pack="true" PackagePath="" />
2324
<None Include="../../../README.md" Pack="true" PackagePath="" />
2425
</ItemGroup>
25-
</Project>
26+
</Project>

‎Src/PChecker/CheckerCore/CheckerMode.cs

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,9 @@ public enum CheckerMode
99
/// Mode for prioritized random search
1010
/// </summary>
1111
BugFinding,
12+
1213
/// <summary>
13-
/// Mode for exhaustive symbolic exploration
14+
/// Mode for P exploration and execution
1415
/// </summary>
15-
Verification,
16-
/// <summary>
17-
/// Mode for exhaustive explicit-state search with state-space coverage reporting
18-
/// </summary>
19-
Coverage
20-
}
16+
PEx
17+
}

‎Src/PChecker/CheckerCore/ExhaustiveEngine.cs

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -74,10 +74,7 @@ private string CreateArguments()
7474
{
7575
switch (_checkerConfiguration.Mode)
7676
{
77-
case CheckerMode.Verification:
78-
arguments.Append("--strategy symbolic ");
79-
break;
80-
case CheckerMode.Coverage:
77+
case CheckerMode.PEx:
8178
arguments.Append($"--strategy {_checkerConfiguration.SchedulingStrategy} ");
8279
break;
8380
default:
@@ -109,7 +106,7 @@ private string CreateArguments()
109106
}
110107
}
111108

112-
arguments.Append($"{_checkerConfiguration.PSymArgs} ");
109+
arguments.Append($"{_checkerConfiguration.CheckerArgs} ");
113110

114111
return arguments.ToString();
115112
}
@@ -234,4 +231,4 @@ public void Run()
234231
}
235232
}
236233
}
237-
}
234+
}

‎Src/PChecker/CheckerCore/Runtime/Logging/IControlledRuntimeLog.cs

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ namespace PChecker.Runtime.Logging
99
{
1010
/// <summary>
1111
/// Interface that allows an external module to track what
12-
/// is happening in the <see cref="ControlledRuntime"/>.
12+
/// is happening in the controlled runtime.
1313
/// </summary>
1414
public interface IControlledRuntimeLog
1515
{
@@ -38,7 +38,6 @@ public interface IControlledRuntimeLog
3838
/// <param name="senderType">The type of the sender, if any.</param>
3939
/// <param name="senderStateName">The state name, if the sender is a state machine, else null.</param>
4040
/// <param name="e">The event being sent.</param>
41-
/// <param name="opGroupId">The id used to identify the send operation.</param>
4241
/// <param name="isTargetHalted">Is the target state machine halted.</param>
4342
void OnSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderStateName,
4443
Event e, bool isTargetHalted);
@@ -241,4 +240,4 @@ void OnMonitorProcessEvent(string monitorType, string stateName, string senderNa
241240
/// </summary>
242241
void OnCompleted();
243242
}
244-
}
243+
}

‎Src/PChecker/CheckerCore/Runtime/Logging/LogWriter.cs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,6 @@ public void LogExecuteAction(StateMachineId id, string handlingStateName, string
9292
/// <param name="senderType">The type of the sender, if any.</param>
9393
/// <param name="senderState">The state name, if the sender is a state machine, else null.</param>
9494
/// <param name="e">The event being sent.</param>
95-
/// <param name="opGroupId">The id used to identify the send operation.</param>
9695
/// <param name="isTargetHalted">Is the target state machine halted.</param>
9796
public void LogSendEvent(StateMachineId targetStateMachineId, string senderName, string senderType, string senderState,
9897
Event e, bool isTargetHalted)
@@ -624,4 +623,4 @@ internal void RemoveLog(IControlledRuntimeLog log)
624623
}
625624
}
626625
}
627-
}
626+
}

‎Src/PChecker/CheckerCore/Runtime/Logging/PCheckerLogJsonFormatter.cs

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -96,10 +96,17 @@ private static object GetEventPayloadInJson(Event e)
9696
return pe.Payload?.ToDict();
9797
}
9898

99+
/// <summary>
100+
/// Called when the log is complete and about to be closed.
101+
/// </summary>
99102
public void OnCompleted()
100103
{
101104
}
102105

106+
/// <summary>
107+
/// Invoked when the specified assertion failure has occurred.
108+
/// </summary>
109+
/// <param name="error">The text of the error.</param>
103110
public void OnAssertionFailure(string error)
104111
{
105112
error = RemoveLogTag(error);
@@ -124,6 +131,11 @@ public void OnCreateStateMachine(StateMachineId id, string creatorName, string c
124131
Writer.AddToLogs(updateVcMap: true);
125132
}
126133

134+
/// <summary>
135+
/// Invoked when the specified state machine is idle and the default event handler is about to be executed.
136+
/// </summary>
137+
/// <param name="id">The id of the state machine that the state will execute in.</param>
138+
/// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
127139
public void OnDefaultEventHandler(StateMachineId id, string stateName)
128140
{
129141
stateName = GetShortName(stateName);
@@ -139,6 +151,12 @@ public void OnDefaultEventHandler(StateMachineId id, string stateName)
139151
Writer.AddToLogs(updateVcMap: true);
140152
}
141153

154+
/// <summary>
155+
/// Invoked when the specified event is dequeued by an state machine.
156+
/// </summary>
157+
/// <param name="id">The id of the state machine that the event is being dequeued by.</param>
158+
/// <param name="stateName">The state name, if the state machine is a state machine and a state exists, else null.</param>
159+
/// <param name="e">The event being dequeued.</param>
142160
public void OnDequeueEvent(StateMachineId id, string stateName, Event e)
143161
{
144162
var eventName = GetEventNameWithPayload(e);
@@ -528,4 +546,4 @@ public void OnStrategyDescription(string strategyName, string description)
528546
Writer.AddToLogs();
529547
}
530548
}
531-
}
549+
}

‎Src/PChecker/CheckerCore/Runtime/StateMachines/Exceptions/OnEventDroppedHandler.cs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
namespace PChecker.Runtime.StateMachines.Exceptions
77
{
88
/// <summary>
9-
/// Handles the <see cref="ControlledRuntime.OnEventDropped"/> event.
9+
/// Handles the event dropped notification.
1010
/// </summary>
1111
public delegate void OnEventDroppedHandler(Event e, StateMachineId target);
12-
}
12+
}

‎Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -519,7 +519,6 @@ private protected Task TryHandleActionInvocationExceptionAsync(Exception ex, str
519519
/// <param name="type">Type of the state machine.</param>
520520
/// <param name="name">Optional name used for logging.</param>
521521
/// <param name="initialEvent">Optional initialization event.</param>
522-
/// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
523522
/// <returns>The unique state machine id.</returns>
524523
protected StateMachineId CreateStateMachine(Type type, string name, Event initialEvent = null) =>
525524
Runtime.CreateStateMachine(null, type, name, initialEvent, this);
@@ -529,8 +528,7 @@ protected StateMachineId CreateStateMachine(Type type, string name, Event initia
529528
/// Sends an asynchronous <see cref="Event"/> to a target.
530529
/// </summary>
531530
/// <param name="target">The target.</param>
532-
/// <param name="e">The event to send.</param>
533-
/// <param name="opGroupId">Optional id that can be used to identify this operation.</param>
531+
/// <param name="ev">The event to send.</param>
534532
public void SendEvent(PMachineValue target, Event ev)
535533
{
536534
Assert(ev != null, $"Machine cannot send a null event. Machine {Id} trying to send null event in state {CurrentStateName}.");
@@ -2063,4 +2061,4 @@ public IgnoreEventsAttribute(params Type[] eventTypes)
20632061
}
20642062
}
20652063
}
2066-
}
2064+
}

‎Src/PChecker/CheckerCore/SystematicTesting/Strategies/Feedback/Coverage/TimelineObserver.cs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,11 @@
77

88
namespace PChecker.Feedback;
99

10-
internal class TimelineObserver: IControlledRuntimeLog
10+
internal class TimelineObserver : IControlledRuntimeLog
1111
{
12-
1312
private HashSet<(string, string, string)> _timelines = new();
1413
private Dictionary<string, HashSet<string>> _allEvents = new();
1514
private Dictionary<string, List<string>> _orderedEvents = new();
16-
private IControlledRuntimeLog _controlledRuntimeLogImplementation;
1715

1816
public static readonly List<(int, int)> Coefficients = new();
1917
public static int NumOfCoefficients = 50;
@@ -188,4 +186,4 @@ public void OnStrategyDescription(string strategyName, string description)
188186
public void OnCompleted()
189187
{
190188
}
191-
}
189+
}

‎Src/PCompiler/CompilerCore/Backend/ICodeGenerator.cs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@ namespace Plang.Compiler.Backend
66
{
77
public interface ICodeGenerator
88
{
9+
public const string GlobalConfigName = "GlobalConfig";
10+
911
/// <summary>
1012
/// Generate target language source files from a P project.
1113
/// </summary>

0 commit comments

Comments
 (0)