====== Lab 3 ======

Implement value search, that is, implement the class lab.ValueSearch.  The API of this class and related classes can be found [[http://www.eecs.yorku.ca/course_archive/2019-20/W/4315/api/search/|here]].  In your implementation, you do not have to keep track of the depth, nor do you have not notify that depth or space limits have been hit.  A jar file containing the remaining classes can be found [[http://www.eecs.yorku.ca/course_archive/2019-20/W/4315/jars/search.jar|here]].

As an example, consider the following class.
<code>
public class Account {
	private double balance;
	
	public Account() {
		this.balance = 0.0;
	}
	
	public double getBalance() {
		return this.balance;
	}
	
	public void deposit(double amount) {
		this.balance += amount;
	}
	
	public void withdraw(double amount) {
		this.balance -= amount;
	}
}
</code>
The above class is used in the following app.
<code>
import java.util.Random;

public class Finances {
	public static void main(String[] args) {
		Account account = new Account();
		
		final int LOW = 2;
		final int MEDIUM = 3;
		final int HIGH = 4;
		
		Random random = new Random();
		account.deposit(random.nextInt(HIGH));
		if (!random.nextBoolean()) {
			account.deposit(random.nextInt(LOW));
			if (random.nextBoolean()) {
				// do nothing
			} else {
				account.withdraw(random.nextInt(MEDIUM));
			}
		} else {
			account.deposit(random.nextInt(MEDIUM));
			if (random.nextBoolean()) {
				// do nothing
			} else {
				account.deposit(random.nextInt(LOW));
			}
		}
		System.out.println("Balance: " + account.getBalance());
	}
}
</code>
To apply JPF to the above app, use the following application properties file.
<code>
# paths
classpath = <directories that contain Finances.class and Account.class>
native_classpath = <directories that contain lab.ValueSearch.class, lab.FieldValueSearch.class, lab.ValuedState.class, lab.ValuedStateSpaceDot.class>

# application
target = Finances
cg.enumerate_random = true

# search strategy
search.class = lab.FieldValueSearch
search.value.classname = lab.Account
search.value.fieldname = balance

# listener
listener = lab.ValuedStateSpaceDot
</code>
When JPF is run on the above application properties file, it produces output similar to the following.
<code>
JavaPathfinder core system v8.0 (rev 32+) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
Traversal.main()

====================================================== search started: 2/3/20 12:44 PM
Balance: 0.0
Balance: 0.0
Balance: 0.0
Balance: -1.0
Balance: -2.0
Balance: 0.0
Balance: 1.0
Balance: 1.0
Balance: 1.0
Balance: 2.0
Balance: 1.0
Balance: 1.0
Balance: 0.0
Balance: -1.0
Balance: 2.0
Balance: 2.0
Balance: 1.0
Balance: 0.0
Balance: 2.0
Balance: 2.0
Balance: 3.0
Balance: 3.0
Balance: 3.0
Balance: 4.0
Balance: 3.0
Balance: 3.0
Balance: 2.0
Balance: 1.0
Balance: 4.0
Balance: 4.0
Balance: 4.0
Balance: 3.0
Balance: 2.0
Balance: 4.0
Balance: 5.0
Balance: 5.0
Balance: 5.0
Balance: 6.0

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=36,visited=46,backtracked=82,end=38
search:             maxDepth=0,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=35
heap:               new=810,released=572,maxLive=352,gcCycles=82
instructions:       4892
max memory:         123MB
loaded code:        classes=64,methods=1486

====================================================== search finished: 2/3/20 12:44 PM
</code>
It also generates a file named statespace.dot that represents the following state space.

{{:value-search.jpg|}}

To receive feedback, submit your search class using the submit command //before// Tuesday February 11:\\
submit 4315 lab3 ValueSearch.java