Skip Navigation
York U: Redefine the PossibleHOME | Current Students | Faculty & Staff | Research | International
Search »FacultiesLibrariesCampus MapsYork U OrganizationDirectorySite Index
Future Students, Alumni & Visitors
lab8

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

lab8 [2016/03/02 16:15]
franck
lab8 [2016/03/03 08:46] (current)
franck
Line 60: Line 60:
That is, JPF reports the maximum amount of nondeterminism (maximum number of outgoing transitions from any state of the system under test). That is, JPF reports the maximum amount of nondeterminism (maximum number of outgoing transitions from any state of the system under test).
Apart from the classes that have been discussed in the lectures, also the class ChoiceGenerator, which is part of the package gov.nasa.jpf.vm, may be useful. Apart from the classes that have been discussed in the lectures, also the class ChoiceGenerator, which is part of the package gov.nasa.jpf.vm, may be useful.
-Try not to hard-code  
-<html> 
-<pre> 
-====================================================== 
-</pre> 
-</html> 
-but use an appropriate method provided by JPF. 
Last modified:
2016/03/03 08:46