# MODEL: Three-agent cost-constrained model with 6 states (s0-s5)

# PURPOSE: COTL cost-bounded model checking example.

# LOGIC: COTL

# DESCRIPTION: CostCGS with propositions r, s, g, h; cost-bounded formulas <coalition><cost>F/G/X/U.

Transition
0 AAB AAC BBB 0 0
0 0 0 0 0 0
0 0 0 0 0 0
0 0 0 0 0 0
0 0 0 0 0 0
0 0 0 0 0 0
Name_State
s0 s1 s2 s3 s4 s5
Initial_State
s0
Costs_for_actions_split
AAC s0$1,1,1
AAB s0$1,1,1
BBB s0$1,1,1
Atomic_propositions
r s g h
Labelling
1 0 0 0
1 1 0 0
0 0 1 0
1 1 1 0
1 1 1 1
0 0 1 1
Number_of_agents
3
