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 <namcao@linutronix.de>
---
 .../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:
-- 
2.39.5

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 <namcao@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:

On Mon, Jul 14, 2025 at 02:18:05PM +0200, Gabriele Monaco wrote:
> 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 <namcao@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

Right. Maybe we can prefix them with "ltl_".

> 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)

Not sure what you mean by .init field, but yes the scripts always generate
all variables, even if they are unused. Let me change the scripts.

> 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.

Yes.

> 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)

Be careful of operator precedence. This rule is also what I would suggest,
but you need parentheses:

    RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply (next SWITCH))

because I think the parser understood your rule as:

    RULE = always ((not (SCHEDULING and next SCHEDULING)) imply (next SWITCH))

Defining an operator precedence rules is on my TODO list. Unfortunately no
theory defines this AFAIK, so it is not obvious how should they be defined.

> but the parser got the two SCHEDULING as two different atoms, so I
> guess I did something I was not supposed to do..

This is just the parser's shortcoming. Currently it thinks that they are
different variables.

> 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?

I hope the above already answered your questions. Let me know if anything
is unclear.

Thanks for the report, I will post some patches to address these problems
with the scripts.

Best regards,
Nam

On Mon, Jul 14, 2025 at 02:42:10PM +0200, Nam Cao wrote:
> On Mon, Jul 14, 2025 at 02:18:05PM +0200, Gabriele Monaco wrote:
> > 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)
> 
> Be careful of operator precedence. This rule is also what I would suggest,
> but you need parentheses:
> 
>     RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply (next SWITCH))

Actually no, this also does not work. You need double 'next':

     RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply (next next SWITCH))

Or if you want to allow some other things to happen inbetween, then:

     RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply (SCHEDULING until SWITCH))

Best regards,
Nam

On Mon, 2025-07-14 at 14:48 +0200, Nam Cao wrote:
> On Mon, Jul 14, 2025 at 02:42:10PM +0200, Nam Cao wrote:
> > On Mon, Jul 14, 2025 at 02:18:05PM +0200, Gabriele Monaco wrote:
> > > 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)
> > 
> > Be careful of operator precedence. This rule is also what I would
> > suggest,
> > but you need parentheses:
> > 
> >     RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply
> > (next SWITCH))
> 
> Actually no, this also does not work. You need double 'next':
> 
>      RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply
> (next next SWITCH))
> 

Thanks! This one seems to work.

> Not sure what you mean by .init field

I meant in ltl2k there's this condition for variable usage but not for
variable definition. I'm not sure exactly what it stands for.
  _fill_start():
	...
	if not node.init:
		continue

But I guess you got what I meant already.

> Btw, I think this "(not X) and (next X)" seems very useful. So we
> could
> define a helper for this, perhaps something like "rising_edge".

Yeah good idea! I see myself mixing up in the future otherwise..
I guess you'd need to define also a falling_edge for its counterpart.
Or perhaps making it more compact as just rising/falling (with good
documentation or references to somewhere defining it).

Also we need to make clear this operator takes 2 instances, so whatever
happens after (next) it needs a double next.

Maybe it gets complicated but in the future we might have also some
nextN (next2, next3, etc. with a sensible limit not to explode the
generated code) or something along the line.

> Thanks for the report, I will post some patches to address these
> problems
> with the scripts.

Great, thanks!
I'd say since those are unrelated and the next works as intended, feel
free to add

Tested-by: Gabriele Monaco <gmonaco@redhat.com>

Thanks again,
Gabriele

On Mon, Jul 14, 2025 at 02:48:04PM +0200, Nam Cao wrote:
>      RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply (next next SWITCH))

Btw, I think this "(not X) and (next X)" seems very useful. So we could
define a helper for this, perhaps something like "rising_edge".

Nam