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

# Examples 15.9 and 15.10, 
#
# computing vector x_oo for the two communicating machines model,
# for property
#
# P_{>1/2} (M2 not transmitting  U  M1 transmitting)
#

CTMC
STATES 8
INIT
  0 : 1
ARCS 8
  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
END
REACHES
  6 : 1
  7 : 1
REACHES AT 0.4
  6 : 1
  7 : 1