EECS4315

User Tools

Site Tools

You are here: Mission Critical Systems » lab8
Trace: • lab8
lab8

Differences

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

Link to this comparison view

Next revision		Previous revision
lab8 [2016/03/02 19:30] – created francklab8 [2016/03/03 13:46] (current) – franck
Line 23: Line 23:
 native_classpath=. native_classpath=.
 listener=AmountOfNonDeterminism listener=AmountOfNonDeterminism
 +cg.enumerate_random=true
 </pre> </pre>
 </html> </html>
Line 58: Line 58:
 </pre> </pre>
 </html> </html>
 +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.
  
lab8.1456947048.txt.gz · Last modified: by franck