Demo3 - Fault Diagnosis and Identification

This demo shows two slightly different automata, Model_A and Model_B, with observable actions $\Sigma^o$ = [a, b, c], and unobservable actions $\Sigma^{un}$ = [f]. The following four propositions presented are logically straightforward and easily reasoned, as they are based on a simple example:

  1. Suffix aaa implies f. For suffix aaa, both Model_A and Model_B identify f, as it can only be observed post-occurrence of f.

  2. Suffix aba does not confirm $f$ in Model_A The sequence $aba$ can occur during normal and fault conditions in Model_A. Therefore, aba does not conclusively suggest f has occurred.

  3. Fault f in Model_A is not 3-Diagnosable. Given that the observation suffix aba, covering three events, occurs in both normal and fault modes of Model_A, it’s impossible to unequivocally diagnose f within this span. Thus, Model_A is not 3-diagnosable.

  4. Fault f in Model_B is 3-Diagnosable. In Model_B, the three-event suffixes [abb, bbb] are exclusive to the normal mode and absent in the fault mode. Conversely, [aaa, aab, aba, bab, baa, bab] are unique to the fault mode. The absence of common suffixes between modes in Model_B guarantees its 3-diagnosability, ensuring accurate fault identification from any three-event sequence.

  5. You can download the models: model_A.xml and model_B.xml.

import pyuppaal
from pyuppaal import UModel

print(pyuppaal.__version__)
pyuppaal.set_verifyta_path(r"C:\Users\10262\Documents\GitHub\cav2024\bin\uppaal64-4.1.26\bin-Windows\verifyta.exe")

1.2.1

1. Fault Identification

Temorary files tmp_identify_id.xml will be saved. For more details, please read the docs of UModel.fault_identification().

  1. Suffix aaa implies f. For suffix aaa, both Model_A and Model_B identify f, as it can only be observed post-occurrence of f.

  2. Suffix aba does not confirm $f$ in Model_A The sequence $aba$ can occur during normal and fault conditions in Model_A. Therefore, aba does not conclusively suggest f has occurred.

m_a, m_b = UModel('model_A.xml'), UModel('model_B.xml')
sigma_o, sigma_un = ['a', 'b', 'c'], ['f']

# identification for fault 'f' with o1 = ['a', 'a', 'a'] and o2 = ['a', 'b', 'a']
o1, o2 = ['a', 'a', 'a'], ['a', 'b', 'a']
res1_a = m_a.fault_identification(o1, fault='f', sigma_o=sigma_o, sigma_un=sigma_un)
res1_b = m_b.fault_identification(o1, fault='f', sigma_o=sigma_o, sigma_un=sigma_un)
print(f"{o1} can identify 'f'. Model A: {res1_a[0]},  Model B: {res1_b[0]}.")
res2_a = m_a.fault_identification(o2, fault='f', sigma_o=sigma_o, sigma_un=sigma_un)
res2_b = m_b.fault_identification(o2, fault='f', sigma_o=sigma_o, sigma_un=sigma_un)
print(f"{o2} can identify 'f'. Model A: {res2_a[0]}, Model B: {res2_b[0]}.")
assert res1_a[0] == True
assert res1_b[0] == True
assert res2_a[0] == False
assert res2_b[0] == True

['a', 'a', 'a'] can identify 'f'. Model A: True,  Model B: True.
['a', 'b', 'a'] can identify 'f'. Model A: False, Model B: True.

2. Fault Diagnosability

Temorary files tmp_diagnosable_suffix_id.xml will be saved. For more details, please read the docs of UModel.fault_diagnosability().

  1. Fault f in Model_A is not 3-Diagnosable. Given that the observation suffix aba, covering three events, occurs in both normal and fault modes of Model_A, it’s impossible to unequivocally diagnose f within this span. Thus, Model_A is not 3-diagnosable.

  2. Fault f in Model_B is 3-Diagnosable. In Model_B, the three-event suffixes [abb, bbb] are exclusive to the normal mode and absent in the fault mode. Conversely, [aaa, aab, aba, bab, baa, bab] are unique to the fault mode. The absence of common suffixes between modes in Model_B guarantees its 3-diagnosability, ensuring accurate fault identification from any three-event sequence.

# n-diagnosability for fault 'f', for n=3
res3_a = m_a.fault_diagnosability(fault='f', n=3, sigma_o=sigma_o, sigma_un=sigma_un)
res3_b = m_b.fault_diagnosability(fault='f', n=3, sigma_o=sigma_o, sigma_un=sigma_un)
print(f"Model A is 3-diagnosable: {res3_a[0]}, reason: {res3_a[1].untime_pattern}.")
print(f"Model B is 3-diagnosable: {res3_b[0]}.")

assert res2_a[0] == False
assert res2_b[0] == True

Model A is 3-diagnosable: False, reason: ['c', 'a', 'b', 'a'].
Model B is 3-diagnosable: True.