Differences

This shows you the differences between two versions of the page.

--- lab6 [2016/02/08 22:33] – created franck
+++ lab6 [2020/02/03 21:07] (current) – franck
@@ Line 1: / Line 1: @@
-Implement a simplified version of breadth first search.  Implement it in a class called BFSearch.  Only add notifications related to SearchListeners (no need for dealing with the attribute done, etcetera).
+====== 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