Commit 29df006
committed
File tree
1,355 files changed
+626558
-54263
lines changed- .github/workflows
- Docs
- docs
- advanced
- PVerifierLanguageExtensions
- pobserve
- example
- manual
- tutorial
- Src
- PChecker/CheckerCore
- Runtime/Values
- SystematicTesting
- Strategies/Feedback/Coverage
- Testing
- PCompiler
- CompilerCore
- Backend
- CSharp
- Debugging
- Java
- PChecker
- PEx
- PObserve
- PVerifier
- Symbolic
- Parser
- TypeChecker
- AST
- Declarations
- Expressions
- Statements
- Types
- PCommandLine
- Options
- Parser
- PEx
- scripts
- src
- main
- java
- META-INF
- pex
- commandline
- runtime
- logger
- machine
- buffer
- eventhandlers
- events
- scheduler
- choice
- explicit
- choiceselector
- strategy
- replay
- utils
- exceptions
- misc
- monitor
- random
- serialize
- values
- exceptions
- resources
- test/java/pex
- PObserve
- Examples
- LockServerPObserve
- src
- main
- PSpec
- java/lockserver/pobserve/parser
- test
- java/lockserver/pobserve
- resources
- LockServer
- src
- main
- java/lockserver/pobservejunit
- constants
- logging
- resources
- test/java/lockserver/pobservejunit
- PObserve
- logging
- PObserveCommons
- config
- checkstyle
- spotbugs
- src
- main/java/pobserve
- commons
- commandline
- config
- exceptions
- logging
- utils
- runtime
- events
- exceptions
- parsers
- values
- test
- java/pobserve
- commons
- utils
- runtime
- ClientServerTraceParser
- testcases
- clientserver
- espressomachine
- failuredetector
- twophasecommit
- resources
- PObserveJavaUnitTest
- src
- main/java/pobserve/junit
- log4j
- utils
- test/java/pobserve/junit
- PObserveRegressionTesting
- config
- checkstyle
- spotbugs
- src
- main/java/pobserve/testing
- parsers
- spec
- pSpecs
- resources/logs
- params
- unit-test-logs
- error-logs
- test_case_2_logs
- test_case_3_logs
- test_case_4_logs
- test_case_5_logs
- test_case_6_logs
- test_case_6_log_10100_50_error_sorted
- test_case_6_log_10100_50_error_unsorted
- test_case_6_log_10200_100_error_sorted
- test_case_6_log_10200_100_error_unsorted
- test_case_6_log_12_1_error_sorted
- test_case_6_log_12_1_error_unsorted
- test_case_6_log_14_2_error_sorted
- test_case_6_log_14_2_error_unsorted
- test_case_7_logs
- test_case_7_log_10050_50_error_sorted
- test_case_7_log_10050_50_error_unsorted
- test_case_7_log_10100_100_error_sorted
- test_case_7_log_10100_100_error_unsorted
- test_case_7_log_11_1_error_sorted
- test_case_7_log_11_1_error_unsorted
- test_case_7_log_12_2_error_sorted
- test_case_7_log_12_2_error_unsorted
- error-messages
- test_case_2_logs
- test_case_3_logs
- test_case_4_logs
- test_case_5_logs
- test_case_6_logs
- test_case_7_logs
- happy-logs
- test_case_2_logs
- test_case_3_logs
- test_case_4_logs
- test_case_5_logs
- test_case_6_logs
- test_case_6_log_10100_50_happy_sorted
- test_case_6_log_10100_50_happy_unsorted
- test_case_6_log_10200_100_happy_sorted
- test_case_6_log_10200_100_happy_unsorted
- test_case_6_log_12_1_happy_sorted
- test_case_6_log_12_1_happy_unsorted
- test_case_6_log_14_2_happy_sorted
- test_case_6_log_14_2_happy_unsorted
- test_case_7_logs
- test_case_7_log_10050_50_happy_sorted
- test_case_7_log_10050_50_happy_unsorted
- test_case_7_log_10100_100_happy_sorted
- test_case_7_log_10100_100_happy_unsorted
- test_case_7_log_11_1_happy_sorted
- test_case_7_log_11_1_happy_unsorted
- test_case_7_log_12_2_happy_sorted
- test_case_7_log_12_2_happy_unsorted
- test/java/pobserve/testing/parsers
- PObserve
- config
- checkstyle
- spotbugs
- src
- main/java/pobserve
- commandline
- paramvalidator
- config
- executor
- logger
- metrics
- report
- source
- file
- socket
- models
- utils
- utils
- resources
- test/java/pobserve
- regressionTesting
- PRuntimes
- PCRuntime
- API
- Core
- LinuxUser
- NuttxUser
- SGXUser
- Trusted
- Untrusted
- WinUser
- PSymRuntime
- Examples
- OLD_CAV
- BoundedAsync
- German
- OSRError
- OSR
- SimplePaxos
- Synthetic
- Counter10
- Counter15
- Counter5
- OPORPerElement10
- OPORPerElement15
- OPORPerElement5
- TokenRingError
- Prt_disabled
- Pt
- TokenRing
- TwoPhaseCommitError
- TwoPhaseCommitMultipleTransactionsError
- TwoPhaseCommitMultipleTransactionsSync
- TwoPhaseCommitMultipleTransactions
- TwoPhaseCommit
- PLDI
- BoundedAsync
- ClientServer
- PSrc
- PTst
- German
- OSR
- RobotDriver
- PSpec
- PSrc
- PTst
- SimplePaxos
- TokenRing
- TwoPhaseCommit
- tests
- PingPongForeign
- pingPongForeign1
- PForeign
- PSrc
- pingPongForeign2
- PForeign
- PSrc
- pingPongForeign3
- PForeign
- PSrc
- PTst
- pingPongForeign4
- PForeign
- PSrc
- PingPong
- SymbolicRegressionTests
- 2PCMult/Correct/TwoPhaseCommitMultipleTransactionsTimerFailure
- FatDFS/Correct
- PingPong
- TwoPhaseCommit
- Integration
- Correct
- BoundedAsync
- German
- OSR
- TokenRing
- TwoPhaseCommitSync
- TwoPhaseCommit
- DynamicError
- OSR
- OriginalTokenRing
- Prt_disabled
- Pt
- TwoPhaseCommitError
- TwoPhaseCommitMultipleTransactions
- Monitors/Correct/TwoPhaseCommit
- Paxos/Correct/SimplePaxos
- Scheduler
- Correct
- ElevatorTerminationBag
- ElevatorTermination
- OneWaySendDuplicate
- OneWaySend
- PingPongDefer
- PingPongTwice
- PingPongWithCtorArgs
- PingPong
- PushPop
- RaiseAndGotoDefer
- RaiseAndGoto
- TwoPhaseCommit
- DynamicError
- ElevatorNontermination
- ElevatorWrongBagSemantics
- Shorter/Correct
- TwoPhaseCommitMultipleTransactionsParticipantFailure
- TwoPhaseCommitMultipleTransactionsParticipantSuccess
- TwoPhaseCommitMultipleTransactionsTimerFailure
- TwoPhaseCommitMultipleTransactionsTimerSuccess
- TwoPhaseCommitMultipleTransactions
- Test/Correct
- TwoPhaseCommitMultipleTransactionsTimerFailure
- TwoPhaseCommitMultipleTransactionsTimerSuccess
- TooLong/Correct
- TwoPhaseCommitMultipleTransactionsLessNondet
- TwoPhaseCommitMultipleTransactions
- scripts
- src
- main/java
- META-INF
- psym
- commandline
- runtime
- logger
- machine
- buffer
- eventhandlers
- events
- scheduler
- replay
- search
- choiceorchestration
- explicit
- symbolic
- symmetry
- taskorchestration
- statistics
- values
- exceptions
- utils
- exception
- monitor
- random
- serialize
- valuesummary
- solvers
- bdd
- sat/expr
- util
- test/java/psym
- Scripts/TutorialsChecker
- Tst
- CorrectLogs/bugs2
- PortfolioTests/TokenRing
- RegressionTests
- Combined/StaticError
- ControlImpureEnclosedFunCalls
- ControlImpureInExit1
- ControlImpureInExit2
- ControlImpureInExit3
- ControlImpureInExit4
- ControlImpureInExit5
- ControlImpureInExit6
- ControlImpureInGoto1
- ControlImpureInGoto2
- ControlImpureInGoto3
- ControlImpureInGoto4
- ControlImpureInGoto5
- ControlImpureInGoto6
- ControlImpureInGoto7
- PopInExitFun
- RaiseInExitFun
- Feature1SMLevelDecls
- Correct
- BugRepro1
- ParamTest
- PingPong
- bug3
- bug4
- DynamicError
- MaxInstances
- ParamTest2
- StaticError
- DeferIgnoreSameEvent
- DeferredNullEvent
- EventDeferredDoSameState
- EventDeferredHandledSameState
- EventDeferredTransDoSameState
- HasEntryArgs
- HasExitArgs
- IgnoredNullEvent
- NonExistentDoFun
- NonExistentEntryFun
- NonExistentExitFun
- NonExistentGotoFun
- NullEventDecl
- ParamTest3
- ParamTest4
- RaisedNullEvent
- SentNullEvent
- Feature2Stmts
- Correct
- pingPongReceive4
- pingPongReceive5
- DynamicError
- GotoStmt1
- GotoStmt2
- pingPongReceive4
- pingPongReceive5
- StaticError
- entryExit
- eventExprSendRaise
- linear3
- Feature3Exprs
- Correct
- ExprOperatorsAsserts
- ModExpr1
- ShortCircuitEval
- DynamicError
- InOperator
- ModExpr1
- StaticError
- ExprsOperators
- InOperator
- Feature4DataTypes
- Correct
- CastInExprsAsserts
- EnumType
- anyTypeNullValue
- nonAtomicDataTypes12
- nonAtomicDataTypes13
- nonAtomicDataTypes16
- nonAtomicDataTypesAllAsserts
- nonAtomicDataTypes
- string0
- stringcomp
- DynamicError
- CastInExprs1
- CastInExprs2
- CastInExprs3
- CastInExprs4
- CastInExprs5
- CastInExprs6
- EnumType1
- anyType1
- anyType2
- anyType3
- anyType
- nonAtomicDataTypes10
- nonAtomicDataTypes11
- nonAtomicDataTypes14
- nonAtomicDataTypes1
- nonAtomicDataTypes2
- nonAtomicDataTypes3
- nonAtomicDataTypes4
- nonAtomicDataTypes5
- nonAtomicDataTypes6
- nonAtomicDataTypes7
- nonAtomicDataTypes8
- nonAtomicDataTypes9
- nonAtomicDataTypes
- StaticError
- CastInExprs
- EnumType
- nonAtomicDataTypes
- string2
- Feature5ModuleSystem/Correct
- ElevatorMod
- Elevator
- OSR
- PingPongDingDongMod
- Integration
- Correct
- PingPongDefer
- PingPongDingDong
- PingPongMonitor
- PingPong
- SEM_OneMachine_18
- SEM_OneMachine_19
- SEM_OneMachine_2
- SEM_OneMachine_31
- SEM_OneMachine_4
- SEM_OneMachine_7
- SEM_TwoMachines_14
- SEM_TwoMachines_1
- SEM_TwoMachines_3
- SEM_TwoMachines_5
- SEM_TwoMachines_7
- SEM_TwoMachines_8
- TokenRing
- openwsn1
- DynamicError
- Actions_1
- Actions_3
- Actions_5
- Actions_6
- Multi_Paxos_3
- Multi_Paxos_4
- PingPongWithCall
- SEM_OneMachine_10
- SEM_OneMachine_11
- SEM_OneMachine_12
- SEM_OneMachine_13
- SEM_OneMachine_14
- SEM_OneMachine_15
- SEM_OneMachine_16
- SEM_OneMachine_1
- SEM_OneMachine_25
- SEM_OneMachine_28
- SEM_OneMachine_32
- SEM_OneMachine_36
- SEM_OneMachine_39
- SEM_OneMachine_3
- SEM_OneMachine_41
- SEM_OneMachine_42
- SEM_OneMachine_5
- SEM_OneMachine_6
- SEM_OneMachine_8
- SEM_OneMachine_9
- SEM_TwoMachines_10
- SEM_TwoMachines_12
- SEM_TwoMachines_15
- SEM_TwoMachines_16
- SEM_TwoMachines_17
- SEM_TwoMachines_18
- SEM_TwoMachines_19
- SEM_TwoMachines_2
- SEM_TwoMachines_4
- SEM_TwoMachines_6
- SEM_TwoMachines_9
- StaticError
- IncludeError
- TokenRing_Typos
- Liveness
- Correct
- Liveness_FAIRNONDET2
- Liveness_FAIRNONDET
- DynamicError
- InfiniteLoopInAtomicBlock
- Liveness_NONDET2
- Liveness_NONDET
- TestParamTester
- 1_ClientServer
- PSpec
- PSrc
- PTst
- Timer
- PSrc
- UnitTests
- Core
- Runners
- TypeChecker
- Tutorial
- 1_ClientServer
- PSrc
- PTst
- 2_TwoPhaseCommit
- PForeign
- PTst
- 3_EspressoMachine/PTst
- 4_FailureDetector/PTst
- 5_Paxos
- PSpec
- PSrc
- PTst
- 6_Raft
- PSpec
- PSrc
- PTst
- Advanced
- 1_ChainReplicationVerification
- PSrc
- 2_TwoPhaseCommitVerification
- KeyValue
- PSrc
- Rounds
- PSrc
- Single
- PSrc
- 3_RingLeaderVerification
- PSrc
- 4_Paxos
- PSrc
- 5_Consensus
- PSrc
- 6_DistributedLock
- PSrc
- 7_ShardedKV
- PSrc
- 8_LockServer
- PSrc
Some content is hidden
Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.
1,355 files changed
+626558
-54263
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
24 | 24 | | |
25 | 25 | | |
26 | 26 | | |
27 | | - | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
| 25 | + | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
Lines changed: 65 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
| 25 | + | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
| 51 | + | |
| 52 | + | |
| 53 | + | |
| 54 | + | |
| 55 | + | |
| 56 | + | |
| 57 | + | |
| 58 | + | |
| 59 | + | |
| 60 | + | |
| 61 | + | |
| 62 | + | |
| 63 | + | |
| 64 | + | |
| 65 | + | |
Lines changed: 41 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
| 25 | + | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | | - | |
2 | | - | |
3 | | - | |
4 | | - | |
| 1 | + | |
5 | 2 | | |
6 | 3 | | |
7 | | - | |
8 | | - | |
| 4 | + | |
| 5 | + | |
9 | 6 | | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
10 | 12 | | |
11 | 13 | | |
12 | | - | |
| 14 | + | |
13 | 15 | | |
| 16 | + | |
14 | 17 | | |
15 | | - | |
16 | | - | |
17 | | - | |
18 | | - | |
19 | | - | |
20 | | - | |
21 | | - | |
22 | | - | |
23 | | - | |
24 | | - | |
25 | | - | |
26 | | - | |
27 | | - | |
28 | | - | |
29 | | - | |
30 | | - | |
31 | | - | |
32 | | - | |
33 | | - | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
| 25 | + | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
| 51 | + | |
| 52 | + | |
| 53 | + | |
| 54 | + | |
| 55 | + | |
| 56 | + | |
| 57 | + | |
| 58 | + | |
| 59 | + | |
| 60 | + | |
| 61 | + | |
| 62 | + | |
| 63 | + | |
| 64 | + | |
| 65 | + | |
| 66 | + | |
| 67 | + | |
| 68 | + | |
| 69 | + | |
| 70 | + | |
| 71 | + | |
| 72 | + | |
| 73 | + | |
| 74 | + | |
| 75 | + | |
| 76 | + | |
| 77 | + | |
| 78 | + | |
| 79 | + | |
| 80 | + | |
| 81 | + | |
| 82 | + | |
| 83 | + | |
| 84 | + | |
| 85 | + | |
| 86 | + | |
| 87 | + | |
| 88 | + | |
| 89 | + | |
| 90 | + | |
| 91 | + | |
| 92 | + | |
| 93 | + | |
| 94 | + | |
| 95 | + | |
| 96 | + | |
| 97 | + | |
| 98 | + | |
| 99 | + | |
| 100 | + | |
| 101 | + | |
| 102 | + | |
| 103 | + | |
| 104 | + | |
| 105 | + | |
| 106 | + | |
| 107 | + | |
| 108 | + | |
| 109 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
| 25 | + | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
| 51 | + | |
| 52 | + | |
| 53 | + | |
| 54 | + | |
| 55 | + | |
| 56 | + | |
| 57 | + | |
| 58 | + | |
| 59 | + | |
| 60 | + | |
| 61 | + | |
| 62 | + | |
| 63 | + | |
| 64 | + | |
| 65 | + | |
| 66 | + | |
| 67 | + | |
| 68 | + | |
| 69 | + | |
| 70 | + | |
| 71 | + | |
| 72 | + | |
| 73 | + | |
| 74 | + | |
| 75 | + | |
| 76 | + | |
| 77 | + | |
| 78 | + | |
0 commit comments