mod PMAUDE is
	pr FLOAT .
	including CONFIGURATION .
	
	sorts Scheduler ScheduleElem ScheduleList .
	subsort ScheduleElem < ScheduleList .
	subsort Scheduler < Configuration .

	op  nil : -> ScheduleList .
	op  _;_ : ScheduleList ScheduleList -> ScheduleList [assoc comm id: nil] .

	op [_,_] : Float Msg -> ScheduleElem .
	op {_|_} : Float ScheduleList -> Scheduler .
	op insert : Scheduler ScheduleElem -> Scheduler .
	op insert : ScheduleList ScheduleElem -> ScheduleList .
	op tick : Scheduler -> Configuration .
	op global-time : Scheduler -> Float .

	var SL : ScheduleList .
	var e : ScheduleElem .
	vars t1 t2 gt : Float .
	vars M1 M2 : Msg .

	eq global-time({ gt | SL }) = gt .
	eq insert({ gt | SL },e) = { gt | insert(SL,e) } .
	eq insert([ t1 , M1 ] ; SL , [ t2 , M2 ]) = if t1 < t2 then [ t1 , M1 ] ; insert(SL, [ t2 , M2 ]) else ([ t2 , M2 ] ; [ t1 , M1 ] ; SL) fi .
	eq insert( nil , e) = e .
	eq tick({ gt | [ t1 , M1 ] ; SL }) = M1 { t1 | SL } .

endm	
	

mod SAMPLER is
  protecting RANDOM .
  protecting COUNTER .
  protecting RAT .
  protecting NAT .
  protecting CONVERSION .

  op sampleExpWithMean : Float -> Float .
  op sampleExpWithRate : Float -> Float .
  op sampleBerWithP : Float -> Bool .
  op sampleNormal : Float Float -> Float .
  op sampleT : Float -> Float .
  op sampleChi : Float -> Float .
  op sampleF : Float Float -> Float .

  op rand : -> Float .
  rl [rnd] : rand => float(random(counter + 1) / 4294967296) .

  var R R1 : Float .

  rl sampleExpWithMean(R) => R * (- log(rand)) .
  rl sampleExpWithRate(R) => (- log(rand)) / R .
  rl sampleBerWithP(R) => if rand < R then true else false fi . 

endm