Package org.mpi_sws.jmc.api.util

Class JmcRandom

java.lang.Object

java.util.Random

org.mpi_sws.jmc.api.util.JmcRandom

All Implemented Interfaces:

Serializable, RandomGenerator

public class JmcRandom
extends Random

A JMC-specific implementation of java.util.Random that allows for model checking. This class overrides the next method to yield control to the JMC runtime, allowing for reactive event handling and model checking.

See Also:

• Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from interface java.util.random.RandomGenerator

RandomGenerator.ArbitrarilyJumpableGenerator, RandomGenerator.JumpableGenerator, RandomGenerator.LeapableGenerator, RandomGenerator.SplittableGenerator, RandomGenerator.StreamableGenerator

Constructor Summary

Constructors

Constructor	Description
JmcRandom()	Default constructor for JmcRandom.
JmcRandom(long seed)	To ensure compatibility with the java.util.Random API, this constructor is provided.

Method Summary

Modifier and Type	Method	Description
int	next(int bits)	This method is overridden to yield control to the JMC runtime.

Methods inherited from class java.util.Random

doubles, doubles, doubles, doubles, from, ints, ints, ints, ints, longs, longs, longs, longs, nextBoolean, nextBytes, nextDouble, nextFloat, nextGaussian, nextInt, nextInt, nextLong, setSeed

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface java.util.random.RandomGenerator

isDeprecated, nextDouble, nextDouble, nextExponential, nextFloat, nextFloat, nextGaussian, nextInt, nextLong, nextLong

Constructor Details

JmcRandom

public JmcRandom()

Default constructor for JmcRandom. Ignores the seed

JmcRandom

public JmcRandom(long seed)

To ensure compatibility with the java.util.Random API, this constructor is provided. Ignores the seed.

Method Details

next

public int next(int bits)

This method is overridden to yield control to the JMC runtime. It allows the JMC model checker to handle reactive events and return a random value.

Overrides:

next in class Random

Parameters:

bits - the number of bits to generate

Returns:

a random integer value based on the specified number of bits