Implement value search, that is, implement the class lab.ValueSearch. The API of this class and related classes can be found 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 here.

As an example, consider the following class.

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;
	}
}

The above class is used in the following app.

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());
	}
}

To apply JPF to the above app, use the following application properties file.

# 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

When JPF is run on the above application properties file, it produces output similar to the following.

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

It also generates a file named statespace.dot that represents the following state space.

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