# /* BRP - iz magisterija */
# /* Robert Meolic, 14. 10. 1999 */

# known model checker's settings
global mc_diagnostic
global mc_explain
global mc_tracepath
global mc_automaton
global mc_minimize
global mc_progress

# use TYPE=1 for raw and onthefly composition
# use TYPE=0 otherwise
set TYPE 1

# set parameters for model checking
set MCPAR [expr !$mc_progress]

pa_read_process "brp.dat"
ccs_read brp.ccs

if {$TYPE == 0} {
  out "PROCESS BRP: "
  out [pa_state_number BRP]
  out " st, "
  out [pa_transition_number BRP]
  out " tr, "
  out [pa_transition_visible BRP]
  outline " vis"
}

if {$TYPE == 1} {
  out "COMPOSITION BRP: "
  out [pa_comp_state_number BRP]
  out " st, "
  out [pa_comp_transition_number BRP]
  out " tr, "
  out [pa_comp_transition_visible BRP]
  outline " vis"
}

outline ""

outline "# 1. Podatkovni paketi se prenasajo neskoncno mnogokrat"
mc_check_actl $TYPE BRP F1 $MCPAR

outline "#2. Prvo sprejeto sporocilo za podatkovni paket je IFST"
mc_check_actl $TYPE BRP F2 $MCPAR

outline "3. Med prenosom podatkovnega paketa dobi prejemnik najvec en IFST"
mc_check_actl $TYPE BRP F3 $MCPAR

outline "4. Zadnje sprejeto sporocilo za podatkovni paket je IOK ali INOK"
mc_check_actl $TYPE BRP F4 $MCPAR

outline "5. IFST in IINC nista zadnji sprejeti sporocili za podatkovni paket"
mc_check_actl $TYPE BRP F5 $MCPAR

outline "6. Enota P ne zacne naslednjega prenosa, dokler ne dobi obvestilo"
mc_check_actl $TYPE BRP F6 $MCPAR

outline "7. Enota P dobi le eno obvestilo za vsak podatkovni paket"
mc_check_actl $TYPE BRP F7 $MCPAR

outline "8. Enota P ne dobi INOK, ce dobi enota C IOK in obratno"
mc_check_actl $TYPE BRP F8 $MCPAR
mc_check_actl $TYPE BRP F9 $MCPAR
mc_check_actl $TYPE BRP F10 $MCPAR
mc_check_actl $TYPE BRP F11 $MCPAR

outline "9. Enota P ne dobi IDK, ce ni prenesen noben kos podatkovnega paketa"
mc_check_actl $TYPE BRP F12 $MCPAR
