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.

Adding Groovy libraries for JPF runs.

Adding options to run.sh for automation.

Adding location.mode variable conflict tracker.

Miscellaneous cleanups.

Fixing a bug in ClassLoader.defineClass(); basically this method has to still return a java.lang.LinkageError exception when it attempts to define the same class twice.

Adding a variable conflict tracker/listener; this is useful for both device and global variable conflict types.

Adding an example groovy SmartThings test of 2 apps.

Adding more memory to the run.

Fixing JPF for methodMissing() method in Groovy: 1) Bug in detecting the array type, 2) Different expected responses for ClassNotFoundException vs. ClassDefNotFoundException.

Moving recursive lookup for defineClass0 just in the native method itself; messing up with the ClassLoaderInfo could potentially harm the URLClassLoader class and other class-loading mechanisms in JPF.