Skip to content
Snippets Groups Projects
Commit 86b219fc authored by Regis Blanc's avatar Regis Blanc
Browse files

use implicit state for random with correct execution

parent 2454f640
No related branches found
No related tags found
No related merge requests found
...@@ -7,30 +7,91 @@ import leon.lang.xlang._ ...@@ -7,30 +7,91 @@ import leon.lang.xlang._
object Random { object Random {
@library
case class State(var seed: BigInt)
@library
def newState: State = State(0)
@library @library
@isabelle.noBody() @isabelle.noBody()
def nextBoolean(): Boolean = epsilon((x: Boolean) => true) def nextBoolean(implicit state: State): Boolean = {
state.seed += 1
nativeNextBoolean
} ensuring((x: Boolean) => true)
@library @library
@extern
@isabelle.noBody() @isabelle.noBody()
def nextInt(): Int = epsilon((x: Int) => true) private def nativeNextBoolean(implicit state: State): Boolean = {
scala.util.Random.nextBoolean
} ensuring((x: Boolean) => true)
@library
@isabelle.noBody()
def nextInt(implicit state: State): Int = {
state.seed += 1
nativeNextInt
} ensuring((x: Int) => true)
@library
@extern
@isabelle.noBody()
private def nativeNextInt(implicit state: State): Int = {
scala.util.Random.nextInt
} ensuring((x: Int) => true)
@library @library
@isabelle.noBody() @isabelle.noBody()
def nextInt(max: Int): Int = { def nextInt(max: Int)(implicit state: State): Int = {
require(max > 0) require(max > 0)
epsilon((x: Int) => x >= 0 && x < max) state.seed += 1
nativeNextInt(max)
} ensuring(res => res >= 0 && res < max) } ensuring(res => res >= 0 && res < max)
@library @library
@extern
@isabelle.noBody() @isabelle.noBody()
def nextBigInt(): BigInt = epsilon((x: BigInt) => true) def nativeNextInt(max: Int)(implicit state: State): Int = {
scala.util.Random.nextInt(max)
} ensuring(res => res >= 0 && res < max)
@library
@isabelle.noBody()
def nextBigInt(implicit state: State): BigInt = {
state.seed += 1
nativeNextBigInt
} ensuring((x: BigInt) => true)
@library @library
@extern
@isabelle.noBody() @isabelle.noBody()
def nextBigInt(max: BigInt): BigInt = { private def nativeNextBigInt(implicit state: State): BigInt = {
BigInt(scala.util.Random.nextInt)
} ensuring((x: BigInt) => true)
@library
@isabelle.noBody()
def nextBigInt(max: BigInt)(implicit state: State): BigInt = {
require(max > 0) require(max > 0)
epsilon((x: BigInt) => x >= 0 && x < max) state.seed += 1
} ensuring(res => res >= 0 && res < max) nativeNextBigInt(max)
} ensuring((res: BigInt) => res >= 0 && res < max)
@library
@extern
@isabelle.noBody()
private def nativeNextBigInt(max: BigInt)(implicit state: State): BigInt = {
BigInt(scala.util.Random.nextInt(max.toInt))
} ensuring((x: BigInt) => x >= 0 && x < max)
} }
...@@ -16,7 +16,7 @@ object DataRacing { ...@@ -16,7 +16,7 @@ object DataRacing {
case class RunnableCons(instr: AtomicInstr, tail: Runnable) extends Runnable case class RunnableCons(instr: AtomicInstr, tail: Runnable) extends Runnable
case class RunnableNil() extends Runnable case class RunnableNil() extends Runnable
def execute(t1: Runnable, t2: Runnable, state: SharedState): Unit = (t1, t2) match { def execute(t1: Runnable, t2: Runnable, state: SharedState)(implicit randomState: Random.State): Unit = (t1, t2) match {
case (RunnableCons(x,xs), RunnableCons(y,ys)) => case (RunnableCons(x,xs), RunnableCons(y,ys)) =>
if(Random.nextBoolean) { if(Random.nextBoolean) {
x.instr(state) x.instr(state)
...@@ -37,6 +37,7 @@ object DataRacing { ...@@ -37,6 +37,7 @@ object DataRacing {
//z3 finds counterexample in 0.5 //z3 finds counterexample in 0.5
//cvc4 needs 130 seconds //cvc4 needs 130 seconds
def main(): Int = { def main(): Int = {
implicit val randomState = Random.newState
val state = SharedState(0) val state = SharedState(0)
val t1 = RunnableCons((s: SharedState) => s.i = s.i + 1, RunnableNil()) val t1 = RunnableCons((s: SharedState) => s.i = s.i + 1, RunnableNil())
val t2 = RunnableCons((s: SharedState) => s.i = s.i * 2, RunnableNil()) val t2 = RunnableCons((s: SharedState) => s.i = s.i * 2, RunnableNil())
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment