IBM®
Skip to main content
    Israel [change]    Terms of use
 
 
 
    Home    Products    Services & solutions    Support & downloads    My account    
IBM Research

RuleBase Parallel Edition

Formal Verification


Generalized Buffer (PSL/Sugar version)

Sender request get acknowledged

vunit sender_req_get_ack 
{
"Sender request get acknowleged"
%for i in 0..3 do
    assert always (StoB_REQ(%{i}) -> eventually! (BtoS_ACK(%{i}))); 
%end
}
Results



 
 





    About IBMPrivacyContact