Graded-CTL NuSMV
Execution Traces
Counterexamples for a simple model | |
|
--specification !E>10 F q is false
Trace Type: Counterexample → Input: 1.1 ← → State: 1.1 ← state = p → Input: 1.2 ← → State: 1.2 ← state = u → Input: 1.3 ← → State: 1.3 ← state = q → Input: 2.2 ← → State: 2.2 ← state = s → Input: 2.3 ← → State: 2.3 ← state = q → Input: 3.1 ← → State: 3.1 ← state = p Loop starts here → Input: 3.2 ← → State: 3.2 ← state = s → Input: 3.3 ← → State: 3.3 ← state = t End loop → Input: 3.4 ← → State: 3.4 ← state = s → Input: 3.5 ← → State: 3.5 ← state = q |
Counterexamples for a more complex model | |
Sender:
Receiver: 
You can find more details about the model here |
--specification !(E>1 G (E >0
F sender.state = get &
E >0 F receiver.state = deliver)) is false Trace Type: Counterexample → Input: 1.1 ← → State: 1.1 ← sender.state = get sender.abp = 0 sender.data = 0 s2r_in.tag = mt s2r_in.data = 0 s2r_out.tag = mt s2r_out.data = 0 receiver.state = receive receiver.abp = 0 receiver.data = 0 r2s_in.tag = mt r2s_out.tag = mt → Input: 1.2 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 1.2 ← sender.state = send → Input: 1.3 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 1.3 ← sender.state = wait_for_ack s2r_in.tag = data0 Loop starts here → Input: 1.4 ← _process_selector_ = s2r running = 0 s2r.running = 1 r2s.running = 0 receiver.running = 0 sender.running = 0 → State: 1.4 ← s2r_in.tag = mt s2r_out.tag = data0 End loop → Input: 1.5 ← _process_selector_ = s2r running = 0 s2r.running = 1 r2s.running = 0 receiver.running = 0 sender.running = 0 → State: 1.5 ← → Input: 1.6 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 1.6 ← s2r_out.tag = mt receiver.state = deliver → Input: 1.7 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 1.7 ← receiver.state = send_ack receiver.abp = 1 → Input: 1.8 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 1.8 ← receiver.state = receive r2s_in.tag = ack0 → Input: 1.9 ← _process_selector_ = r2s running = 0 s2r.running = 0 r2s.running = 1 receiver.running = 0 sender.running = 0 → State: 1.9 ← r2s_in.tag = mt r2s_out.tag = ack0 → Input: 1.10 ← _process_selector_ = r2s running = 0 s2r.running = 0 r2s.running = 1 receiver.running = 0 sender.running = 0 → State: 1.10 ← → Input: 1.11 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 1.11 ← → Input: 1.12 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 1.12 ← sender.state = get sender.abp = 1 r2s_out.tag = mt → Input: 1.13 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 1.13 ← sender.state = send → Input: 1.14 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 1.14 ← sender.state = wait_for_ack s2r_in.tag = data1 → Input: 1.15 ← _process_selector_ = s2r running = 0 s2r.running = 1 r2s.running = 0 receiver.running = 0 sender.running = 0 → State: 1.15 ← s2r_in.tag = mt s2r_out.tag = data1 → Input: 1.16 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 1.16 ← s2r_out.tag = mt receiver.state = deliver → Input: 1.17 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 1.17 ← receiver.state = send_ack receiver.abp = 0 → Input: 1.18 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 1.18 ← receiver.state = receive r2s_in.tag = ack1 → Input: 1.19 ← _process_selector_ = r2s running = 0 s2r.running = 0 r2s.running = 1 receiver.running = 0 sender.running = 0 → State: 1.19 ← r2s_in.tag = mt r2s_out.tag = ack1 → Input: 1.20 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 1.20 ← sender.state = get sender.abp = 0 r2s_out.tag = mt → Input: 1.21 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 1.21 ← sender.state = send Loop starts here → Input: 2.1 ← → State: 2.1 ← sender.state = get sender.abp = 0 sender.data = 0 s2r_in.tag = mt s2r_in.data = 0 s2r_out.tag = mt s2r_out.data = 0 receiver.state = receive receiver.abp = 0 receiver.data = 0 r2s_in.tag = mt r2s_out.tag = mt End loop → Input: 2.2 ← _process_selector_ = s2r running = 0 s2r.running = 1 r2s.running = 0 receiver.running = 0 sender.running = 0 → State: 2.2 ← → Input: 2.3 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 2.3 ← sender.state = send → Input: 2.4 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 2.4 ← sender.state = wait_for_ack s2r_in.tag = data0 → Input: 2.5 ← _process_selector_ = s2r running = 0 s2r.running = 1 r2s.running = 0 receiver.running = 0 sender.running = 0 → State: 2.5 ← s2r_in.tag = mt s2r_out.tag = data0 → Input: 2.6 ← _process_selector_ = s2r running = 0 s2r.running = 1 r2s.running = 0 receiver.running = 0 sender.running = 0 → State: 2.6 ← → Input: 2.7 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 2.7 ← s2r_out.tag = mt receiver.state = deliver → Input: 2.8 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 2.8 ← receiver.state = send_ack receiver.abp = 1 → Input: 2.9 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 2.9 ← receiver.state = receive r2s_in.tag = ack0 → Input: 2.10 ← _process_selector_ = r2s running = 0 s2r.running = 0 r2s.running = 1 receiver.running = 0 sender.running = 0 → State: 2.10 ← r2s_in.tag = mt r2s_out.tag = ack0 → Input: 2.11 ← _process_selector_ = r2s running = 0 s2r.running = 0 r2s.running = 1 receiver.running = 0 sender.running = 0 → State: 2.11 ← → Input: 2.12 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 2.12 ← → Input: 2.13 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 2.13 ← sender.state = get sender.abp = 1 r2s_out.tag = mt → Input: 2.14 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 2.14 ← sender.state = send → Input: 2.15 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 2.15 ← sender.state = wait_for_ack s2r_in.tag = data1 → Input: 2.16 ← _process_selector_ = s2r running = 0 s2r.running = 1 r2s.running = 0 receiver.running = 0 sender.running = 0 → State: 2.16 ← s2r_in.tag = mt s2r_out.tag = data1 → Input: 2.17 ← _process_selector_ = receiver running = 0 s2r.running = 0v r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 2.17 ← s2r_out.tag = mt receiver.state = deliver → Input: 2.18 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 2.18 ← receiver.state = send_ack receiver.abp = 0 → Input: 2.19 ← _process_selector_ = receiver running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 1 sender.running = 0 → State: 2.19 ← receiver.state = receive r2s_in.tag = ack1 → Input: 2.20 ← _process_selector_ = r2s running = 0 s2r.running = 0 r2s.running = 1 receiver.running = 0 sender.running = 0 → State: 2.20 ← r2s_in.tag = mt r2s_out.tag = ack1 → Input: 2.21 ← _process_selector_ = sender running = 0 s2r.running = 0 r2s.running = 0 receiver.running = 0 sender.running = 1 → State: 2.21 ← sender.state = get sender.abp = 0 r2s_out.tag = mt |