== Lock model of RTEMS lock in Java, to be used with Java Pathfinder == Code needs to be compiled against jpf.jar (for using Verify). Model needs to be "executed" in JPF.