RLTL model checking support#20
Draft
imnaseer wants to merge 4 commits into
Draft
Conversation
The agent/starter/ExampleTests.csproj is a standalone template with inline Version attributes, which conflicts with the repo's Central Package Management. Exclude agent/** from the docfx project glob. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Port the full symbolic RLTL model-checking engine (~70 core files) from BraggerSpecs to Accordant, adding temporal logic verification capabilities to the framework. New projects: - Accordant.ModelChecking (netstandard2.0): core symbolic engine with ERE, LTL, RLTL derivatives, ABW/NBW automata, alternation elimination, nested DFS / SCC emptiness checking, and StateProp bridge layer - Accordant.ModelChecking.Bdd (net8.0): BDD backend for precise predicate algebra decisions (auto-registers via ModuleInitializer) User-facing API (Properties<T>): - p.Observe(s => predicate, name) creates unified Observation atoms - p.Always/Eventually/LeadsTo/InfinitelyOften/Trigger combinators - RegexPattern with Star/Then/Plus/Optional/Fusion for RLTL regex-prefix - graph.Check(formula) extension method on StateGraphNode Adaptations from BraggerSpecs: - State -> IState throughout (Accordant uses interface) - CloneInternal(Dictionary<object,object>) signature - StringRepresentationInternal with forceRecompute param - Lock() -> Freeze(), removed StepFunctionIdHash - All sample states use [State] attribute with source generator Test coverage (1,050 passing): - 766 core engine unit tests (ERE, RLTL, ABW, NBW, emptiness, fairness, canonicalization, derivatives, equivalence, etc.) - 5 sample projects: Peterson (8), AlternatingBit (25), DiningPhilosophers (37), Paxos (11), EWD998/TerminationDetection (38) Not ported (deferred by design): - EREQ (quantified regex extensions) - Z3 backend - BuchiVisualization / DotRenderer - Terms / SMT-LIB symbolic program layer Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Include Accordant.ModelChecking.dll/.pdb (netstandard2.0) so the RLTL model-checking + LTL/RLTL support ships in the package. The optional net8.0 Bdd backend is not required (the pipeline falls back to the propositional StatePropEba). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.