need_resp.symon

#!/usr/local/bin/symon -dnf
###############################################################
# Name
#  need_resp.symon
#
# Description
#  After an event A with a specific ID, we should receive a response B with the same ID within 5 time units.
#
#  For instance, for the following input, symon detects an error for x0 == hoge3 and x0 == hoge0.
#   A hoge1 3
#   A hoge0 4
#   B hoge1 5
#   A hoge2 6
#   A hoge3 7
#   B hoge2 8
#   B hoge3 13
#
# Usage
#  symon -dnf need_resp.symon -i log.txt
# 
# Author
#  Masaki Waga
###############################################################


var {
    # We define a string parameter to represent the current ID.
    current_id: string;
}

signature A {
    id: string;
}

signature B {
    id: string;
}

# A subexpression that ignores irrelevant A and B signatures.
expr ignore_irrelevant {
    zero_or_more {
        one_of {
            A( id | id != current_id )
        } or {
             B( id | id != current_id )
        }
    }
}

# Ignore the A and B signatures that do not match the current_id.
ignore_irrelevant;
# Match the A signature that matches the current_id.
A( id | id == current_id );
# We only have irrelevant A and B signatures for more than 5 time units, i.e., we have no relevant B within 5 time units.
within (> 5) {
    within (<= 5) {
        ignore_irrelevant
    };
    one_of {
        A( id )
    } or {
        B( id )
    }
}