# $Id: 2comm2.ctmc 609 2007-03-15 17:07:17Z asminer $

# Example 15.11, 
#
# computing vector x_0.4 for the two communicating machines model,
# for property
#
# P_{>1/5} (M2 not transmitting  U^[0.4, 0.4]  M1 transmitting)
#

CTMC
STATES 8
INIT
  0 : 1
ARCS 10
  0 : 1 : 0.9 	# L2
  0 : 3 : 1.0	# L1
  1 : 2 : 3.5	# M2
  1 : 4 : 1.0	# L1
  3 : 4 : 0.9	# L2
  3 : 6 : 3.0	# M1
  4 : 5 : 3.5	# M2
  4 : 7 : 3.0	# M1
  6 : 0 : 5.0   # G1
  7 : 1 : 5.0   # G2
END
REACHES AT 0.4
  6 : 1
  7 : 1