Hanfor's Specification Language

[Eevan-zq]

Hello hauff,
I have two questions. First, if you look at the red underlined sentences in the following figure, I want to know the difference between "Once EXPR becomes satisfied, ..." and "If EXPR holds, ..." (My understanding is that Once EXPR stands for the occurrence of an event, and if EXPR stands for the state of a variable is true). In my understanding, there is little difference between the two.

The second question is whether it can be directly extended in pattern.py when extending the pattern of hanfor.

[hauff]

Hello @Eevan-zq,

regarding your first question:

Yes, you are right there is a difference between the two patterns

• EdgeResponseBoundL2
  Globally, it is always the case that once "R" becomes satisfied, "S" holds for at least "5" time units
• InvarianceBoundL2
  Globally, it is always the case that if "R" holds, then "S" holds for at least "5" time units

The pattern EdgeResponseBoundL2 requires a rising edge for the observable R, which means that its valuation alters from false to true.
The pattern InvarianceBoundL2 does not require a rising edge for the observable R, which means that the precondition of this pattern is fulfilled whenever R evaluates to true.

The EXPR can be replaced by a boolean expression over observables, which means it always evaluates either to true or to false.

[hauff]

@Eevan-zq

Regarding your second question:

I'm not sure that I understand what you are trying to do, so I think it would be error-prone to answer yes or no to this question at this time.

Perhaps you can give me some more information about your extension?

[Eevan-zq]

So my second question is that if I want to formalise this requirement: "if P holds for less than 3s, then Q holds at least 10s."
And you know that there is no pattern which hanfor specification language can use. So if I want add this pattern likes "If EXPR holds for at most DURATION, then EXPR holds afterwards for at least DURATION" and how can I do it ?