contrib/fsm_checker/FD_CHECK/fd.sm

   1
   2
   3 %start Map1::Start
   4 %class fd
   5 %header fd.h
   6
   7 %map Map1
   8 %%
   9 //STATE         TRANSITION                              END STATE       ACTION(S)
  10
  11 Start
  12 {
  13                 fs_close(pid: int, fd: int)
  14                         CloseState
  15                         {save_args(pid, fd);}
  16
  17
  18                 process_exit(pid: int, i: int)
  19                         [my_process_exit(ctxt, pid) == 1]
  20                         ExitState
  21                         {destroy_scenario(i);}
  22
  23                 Default
  24                         Start
  25                         {}
  26
  27 }
  28
  29 CloseState
  30 {
  31         fs_read(pid: int, fd: int, ts_sec: long, ts_nsec: long)
  32                 [test_args(ctxt,pid, fd) == 1]
  33                 CloseState
  34                 {warning("Trying to read from a closed fd");print_ts(ts_sec, ts_nsec); skip_FSM();}
  35
  36         fs_write(pid: int, fd: int)
  37                 [test_args(ctxt,pid, fd) == 1]
  38                 CloseState
  39                 {warning("Trying to write to a closed fd");skip_FSM();}
  40
  41         process_exit(pid: int, i: int)
  42                 [my_process_exit(ctxt, pid) == 1]
  43                 ExitState
  44                 {destroy_scenario(i);}
  45
  46         fs_open(pid: int, fd: int, i: int)
  47                 [test_args(ctxt, pid, fd)==1]
  48                 ExitState
  49                 {destroy_scenario(i);skip_FSM();}
  50
  51         fs_dup3(pid: int, newfd: int, i: int)
  52                 [test_args(ctxt, pid, newfd)==1]
  53                 ExitState
  54                 {destroy_scenario(i);skip_FSM();}
  55
  56         Default CloseState {}
  57 }
  58
  59 ExitState
  60 {
  61         Default ExitState {}
  62 }
  63
  64 %%
  65