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.

Fixing a typo in option name.

Updating main.jpf; Cleaning up the StateReducer.

First version of the StateReducer class.

Adding cameras.

Checking for null value before storing the first write.

Changing main.jpf

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

Adding a new variable.

Adding a new conflict variable.

Adding a null value filter in the tracker; Adding a new conflict variable for lights.

Adding conflict variable for Speeches.

More state reduction

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

Small improvment in state reduction

Adding conflict variables for lights.

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

edits

Adding a condition to not check for timeout when it is 0.

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

Adding new stuff to main.jpf.

SmartThings specific support to reduce state space

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

SmartThings support

Making sure that the timeout feature exits gracefully.

Adding a timeout feature.

Add constanttime class

Adding extract script for libraries.

Fixing a bug in the tracker.

Adding more groups.

Adding a new library into the runtime path.

Adding a missing library.

Updating conflict variables list in main.jpf.

Adding tracked variables in main.jpf.