Co-authored-by: Christine Zhou <zhouchrs@amazon.com>

# Conflicts:
#	Src/PCompiler/CompilerCore/Backend/Symbolic/CompilationContext.cs
#	Src/PCompiler/CompilerCore/Backend/Symbolic/SymbolicCodeGenerator.cs

* 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 <ericjhua@amazon.com>

* [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 <ankushdesai@users.noreply.github.com>

* 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 <goelaman@amazon.com>
Co-authored-by: Eric Hua <eric.hua9146@gmail.com>
Co-authored-by: Eric Hua <ericjhua@amazon.com>
Co-authored-by: mchadalavada <140562632+mchadalavada@users.noreply.github.com>
Co-authored-by: Aishwarya Jagarapu <aishuj@amazon.com>
Co-authored-by: aishu-j <98783691+aishu-j@users.noreply.github.com>
Co-authored-by: ChristineZh0u <48167738+ChristineZh0u@users.noreply.github.com>
Co-authored-by: Zhe Zhou <zorichzorich@gmail.com>