Printing out the number of transitions.

Fixing a bug: misunderstood how the VOD graph is supposed to be generated; we basically track the transitions that produce new states.

Testing DPORStateReducer and ConflictTracker: JPF seems to work fine and find the conflicts.

Fixing a bug: java LinkedList needs removeFirst(), not getFirst() to get and remove a node from the queue.

Fixing a bug: VOD graph traversal should continue with the next neighbor when there is a loop (repeated node found).

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Fixing a bug: restorable state has to be saved when backtrack point info is saved to get the appropriate CG type when restoring.

Optimization: Compare just the state and the fist event/choice of the trace to not repeat the same backtrack trace twice (the two will map to the same state and the algorithm will stop the second execution, so there is no need to record and explore it twice, e.g., the traces 2 0 1 3 and 2 1 0 3 at state 3.

Changing approach: Using vm.restoreState() method to restore JPF to the desired state when backtracking; everything looks correct but probably needs more tests.

Committing a version that almost works: bug to fix is that when an execution finishes and the first backtrack point requires to get back to a higher state, there is no mechanism to roll back to that state.

First part of boolean flip seems to be clean; need to debug the second part and figure out what to do when the current state is lower than the highest state ID for backtrack.

Fixing a potential bug: we now store the event number in the ArrayList together with the list of CGs for backtracking; getting the event number directly from the current array might be misleading because the array choices might have been modified for fair-scheduling.

Cleaning up and fixing bugs; new DPOR implementation seems to be correct; need to test with other pairs.

Fixing a bug: we need to start choiceCounter from 1 instead of 0 for subsequent executions since the first CG (number 0) is the backtrack CG itself.

Reimplementing DPOR Phase 3: Architecting the subsequent executions (backtrack points); need to test how CGs are explored with the current DFSearch.

Reimplementing DPOR Phase 2: VOD graph building and traversal; completing R/W and conflict analysis; cleaning up and refactoring.

Reimplementing DPOR Phase 1: First trace execution, cycle detection, R/W field access analysis.

Starting a new DPOR implementation.

Cleaning up and refactoring.

Fixing bugs: capturing object accesses (read/write) in iterators.

Fixing a bug: off-by-one error in the executed trace checking.

Re-checking and cleaning up the code: most likely still have a bug in re-ordering the two apps.

Adding the old tracker variable for debugging/testing purposes.

Fixing bugs and cleaning up: Continuing sub-graph executions when there is no matched states or cycles that contain all events; checking in the old ConflictTracker for testing.

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Fixing bugs and cleaning up: making sure that the execution of the first trace has fair-scheduling with appropriate state-matching.

Making analysis compatible with infra

Making analysis compatible with new infrastructure

Cleaning up: Removing the full-blown graph traversal.

Cleaning up, fixing bugs---commented out full-blown graph traversal code.

Refactoring; Finding cycles without traversing the entire state graph.

Fixing bugs: moving VOD-graph building into the CGAdvanced method to have the most up-to-date values.

Adding graph traversal to find cycles; adding debug mode for ConflictTracker.

Some fixes for the DPOR state-reducer.

Fixing a bug: merging the analysis part for locationMode w.r.t manual interaction flag.

Fix for a bug in finding the right integer values in the stack frame: need to find a value that's not 0 in the frame (previously we only look at offset 0 or 1 because of adapting the function getValue() from a listener for Java code).

Adding attributes for dimmers.

Code to print graph to output so that dot can be used to generate pdf of graph.

Adding manual transactions to the conflict tracker

Slight changes for safeguard.

Fixing an out of bound bug.

JPF ready to run with old infrastructure

Adding a prevChoiceValue class property to store the previous choice to update the VOD graph correctly.

Attempting state-based DPOR implementation from the SPIN paper.

Adding the first implementation of visible operation dependency graph for stateful DPOR: need to do more test to make sure that it's really working.

Make updates and not edges have manual property

Clean up comments

Rewrite of Conflict Tracker

A change in updateTheOutSet in conflict tracker analysis

A change in propagate method.

Fixing a bug in Conflict Tracker + Make propagate method much simpler

Make a change in ConflictTracker analysis

Compacting the methods

A change in propagate the change method

Make the analysis more efficient

Fixing a small bug in Conflict Tracker

Fixing bugs in Conflict Tracker

Fixing a bug

Fixing a bug in checkForConflict method in Conflict Tracker analysis!

Fixing a bug in manual_write-non_conflict + setSet conflicts

Fixing a bug in Conflict Tracker analysis

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Fixing bug: completing missing/unexplored event combinations.

Change in Analysis

Change in conflict tracker!

Change in listener

Change in the Conflict Tracker analysis

A minor change in ConflictTracker.java

Minor bug fix in ConflictTracker.java

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Fixing a bug in ConflictTracker.java

Code refactoring for sleep set and persistent set analyses.

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Implementing the sleep-set technique for the previous version to explore less combinations of events.

Minor changes in ConflictTracker

Fix a bug in ConflictTracker

Fix a bug in ConflictTracker.java

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Checking in (1) StateReducer, and (2) StateReducerEfficient; ISSUE: the StateReducerEfficient doesn't traverse the sub-graphs completely and JPF ignores some of the child CGs---incomplete POR.

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Make some changes in ConflictTracker listener.

Fixing a bug: wrong CGs were reset when recursing into a sub-graph.

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Completing POR implementation with complete recursions.

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Modifying conflict tracker

Further excluding infrastructure/library field accesses.

Fixing issues: counter bugs, object ID comparison, exclusion of non-event and non-app field sharing.

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

Adding more restrictions in conflict analysis: not to analyze fields from the Groovy library.

Fixing a bug in ConflictTracker.java

Detecting location mode read/write using the old method.

Fixing a bug in listener!

Add required variables of the new listener to the config file.

Add the ConflictTracker to the main branch

More subtle changes to config file and state reducer listener.

Fixing a few bugs. Still need to check for the backtrack analysis.

First version of POR; need to double check the backtrack set analysis.

Adding more state reduction analysis.

Adding the option to activate beam search: a HeuristicSearch with a state queue that is reset at each level.