On Fri, 2025-07-11 at 15:17 +0200, Nam Cao wrote:
> The 'next' operator is a unary operator. It is defined as: "next
> time, the
> operand must be true".
>
> Support this operator. For RV monitors, "next time" means the next
> invocation of ltl_validate().
>
> Signed-off-by: Nam Cao <nam...@linutronix.de>
Hi Nam,
thanks for the series, I did a very stupid test like this:
RULE = always (SCHEDULING imply next SWITCH)
Despite the monitor working or not, the generator created code that
doesn't build, specifically:
1. It creates a variable named switch
- sure I could change the name, but perhaps we could prepend
something to make sure local variables are not C keywords
2. It created unused variables in ltl_start
- _fill_atom_values creates all variables but _fill_start uses only
those where the .init field is true (maybe the model is wrong though)
Now, this specific model reports errors without the sched_switch_vain
tracepoint which I'm introducing in another patch.
For it to work, I have to define it in such a way that scheduling
becomes true at schedule_entry and becomes false right after the
switch:
schedule_entry
SCHEDULING=true
sched_switch
SWITCH=true
schedule_exit
SCHEDULING=false
SWITCH=false
If I understood correctly that's intended behaviour since swapping the
assignments in schedule_exit (or doing a pulse in sched_switch) would
add another event when scheduling is true, which is against the next
requirement.
Now I can't think of a way to rewrite the model to allow a pulse in
sched_switch, that is /whenever scheduling turns to true, the next
event is a switch/ instead of /any time scheduling is true, the next
event is a switch/.
I tried something like:
RULE = always ((not SCHEDULING and next SCHEDULING) imply next
SWITCH)
but the parser got the two SCHEDULING as two different atoms, so I
guess I did something I was not supposed to do..
Is the next operator only meaningful for atoms that are mutually
exclusive (e.g. RED next GREEN, if GREEN is true RED turns to false)
and/or when playing with ltl_atom_set without triggering validations?
What am I missing here?
Thanks,
Gabriele
> ---
> .../trace/rv/linear_temporal_logic.rst | 1 +
> tools/verification/rvgen/rvgen/ltl2ba.py | 26
> +++++++++++++++++++
> 2 files changed, 27 insertions(+)
>
> diff --git a/Documentation/trace/rv/linear_temporal_logic.rst
> b/Documentation/trace/rv/linear_temporal_logic.rst
> index 57f107fcf6dd..9eee09d9cacf 100644
> --- a/Documentation/trace/rv/linear_temporal_logic.rst
> +++ b/Documentation/trace/rv/linear_temporal_logic.rst
> @@ -41,6 +41,7 @@ Operands (opd):
> Unary Operators (unop):
> always
> eventually
> + next
> not
>
> Binary Operators (binop):
> diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py
> b/tools/verification/rvgen/rvgen/ltl2ba.py
> index d11840af7f5f..f14e6760ac3d 100644
> --- a/tools/verification/rvgen/rvgen/ltl2ba.py
> +++ b/tools/verification/rvgen/rvgen/ltl2ba.py
> @@ -19,6 +19,7 @@ from ply.yacc import yacc
> # Unary Operators (unop):
> # always
> # eventually
> +# next
> # not
> #
> # Binary Operators (binop):
> @@ -35,6 +36,7 @@ tokens = (
> 'UNTIL',
> 'ALWAYS',
> 'EVENTUALLY',
> + 'NEXT',
> 'VARIABLE',
> 'LITERAL',
> 'NOT',
> @@ -48,6 +50,7 @@ t_OR = r'or'
> t_IMPLY = r'imply'
> t_UNTIL = r'until'
> t_ALWAYS = r'always'
> +t_NEXT = r'next'
> t_EVENTUALLY = r'eventually'
> t_VARIABLE = r'[A-Z_0-9]+'
> t_LITERAL = r'true|false'
> @@ -327,6 +330,26 @@ class AlwaysOp(UnaryOp):
> # ![]F == <>(!F)
> return EventuallyOp(self.child.negate()).normalize()
>
> +class NextOp(UnaryOp):
> + def normalize(self):
> + return self
> +
> + def _is_temporal(self):
> + return True
> +
> + def negate(self):
> + # not (next A) == next (not A)
> + self.child = self.child.negate()
> + return self
> +
> + @staticmethod
> + def expand(n: ASTNode, node: GraphNode, node_set) ->
> set[GraphNode]:
> + tmp = GraphNode(node.incoming,
> + node.new,
> + node.old | {n},
> + node.next | {n.op.child})
> + return tmp.expand(node_set)
> +
> class NotOp(UnaryOp):
> def __str__(self):
> return "!" + str(self.child)
> @@ -452,12 +475,15 @@ def p_unop(p):
> '''
> unop : ALWAYS ltl
> | EVENTUALLY ltl
> + | NEXT ltl
> | NOT ltl
> '''
> if p[1] == "always":
> op = AlwaysOp(p[2])
> elif p[1] == "eventually":
> op = EventuallyOp(p[2])
> + elif p[1] == "next":
> + op = NextOp(p[2])
> elif p[1] == "not":
> op = NotOp(p[2])
> else:
