Merge branch 'develop-diagram-check-negate' into develop. Close #318.

**Description**

The current diagram to state machine generator notifies with a trigger
if the current state machines the expectation, rather than the opposite.
As the most common use case of that checker is to detect invalid
transitions, rather than valid ones, we want to modify the condition to
check if the current state differs the expectation.

**Type**

- Feature: Produce code in the diagram backend for more common use case.

**Additional context**

None.

**Requester**

- Ivan Perez.

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

When the diagram backend uses the `check` mode, the condition for the
monitor's trigger checks if the states differ, rather than the opposite.

The following Dockerfile uses the diagrams to state machine backend to
produce, from a simple diagram, a check that a given state and input
transition accordingly with state machine, and then compiles the
resulting code with a main that implements the state transitions
manually, after which it prints the message "Success":

```
--- Dockerfile-verify-318
FROM ubuntu:22.04

ENV DEBIAN_FRONTEND=noninteractive

RUN apt-get update
SHELL ["/bin/bash", "-c"]

RUN apt-get install --yes ghc cabal-install libz-dev pkg-config g++

WORKDIR /root/

ENV PATH=/root/.cabal-sandbox/bin:$PATH

RUN cabal update
RUN cabal v1-sandbox init
RUN cabal v1-install alex happy
RUN cabal v1-install BNFC
RUN cabal v1-install copilot-4.6
RUN apt-get install --yes git
RUN apt-get install --yes libbz2-dev libexpat1-dev

ADD diagram-copilot.dot /tmp/
ADD main.c /tmp/

CMD git clone $REPO \
  && pushd $NAME \
  && git checkout $COMMIT \
  && popd \
  && cabal v1-install --force-reinstalls $NAME/ogma-**/ \
  && ogma diagram -p literal -f dot --file-name /tmp/diagram-copilot.dot \
  && cabal v1-exec -- runhaskell copilot/Copilot.hs \
  && gcc /tmp/main.c monitor.c -I . -o main \
  && ./main \
  && echo "Success"

--- diagram-copilot.dot
digraph g{
   rankdir="LR";
   edge[splines="curved"]
   0 -> 0 [label = "input >= 120 && input <= 180"];

   0 -> 1 [label = "input > 180"];
   1 -> 0 [label = "input <= 180"];

   1 -> 1 [label = "input > 180"];

   0 -> 2 [label = "input < 120"];
   2 -> 0 [label = "input >= 120"];

   2 -> 2 [label = "input < 120"];
}

--- main.c
#include <stdio.h>
#include <stdio.h>
#include <stdint.h>
#include <stdlib.h>

#include "monitor.h"

uint8_t input = 150;
uint8_t state = 0;

void handler(uint8_t handler_arg0, uint8_t handler_arg1, uint8_t handler_arg2)
{
  printf("[Calculated] Expected state: %d, Actual State: %d, Input: %d\n",
         handler_arg0, handler_arg1, handler_arg2);
  exit(1);
}

void main (int argc, char **argv)
{
  // We step again with no changes. The machine should remain in state 0.
  step();

  // We step again. The machine should now transition to state 1.
  input = 185;
  state = 1;
  step();

  // We step again with no changes. The machine should remain in state 1.
  state = 1;
  step();

  // We step again. The machine should now transition to state 0.
  input = 110;
  state = 0;
  step();

  // We step again with no changes. The machine should transition to state 2.
  state = 2;
  step();

  // We step again with no changes. The machine should remain in state 2.
  step();

  // We step again. The machine should now transition to state 0.
  input = 185;
  state = 0;
  step();
}
```

Command (substitute variables based on new path after merge):
```sh
$ docker run -e "REPO=https://github.com/NASA/ogma" -e "NAME=ogma" -e "COMMIT=<HASH>" -it ogma-verify-318
```

**Solution implemented**

Modify the diagram backend to use as condition that the current state
and the expectation are different.

**Further notes**

None.

Author: ivanperez-keera

ogma-core/CHANGELOG.md

@@ -3,6 +3,7 @@
 ## [1.X.Y] - 2025-11-21
 
 * Make state machine code return the current state (#317).
+* Negate condition in state machine monitor (#318).
 
 ## [1.10.0] - 2025-09-21
 

ogma-core/src/Command/Diagram.hs

@@ -406,7 +406,7 @@ diagramToCopilot diag mode = (machine, arguments)
 
     -- Elements of the spec.
     propExpr     = case mode of
-                     CheckState   -> "stateMachine1 == externalState"
+                     CheckState   -> "stateMachine1 /= externalState"
                      ComputeState -> "true"
                      CheckMoves   -> "true"
     initialState = minimum states