NuSMV development : Change the Function of "TRUE" in case statement

Recently I have tried to do some work in translating some models into Nusmv models, but I wanna try to change the function of "TRUE:" keyword. As we all know, the "TRUE:" in "case ... esac;" can define some actions you want when the case conditions do not have that specific condition, however, I have the requirement that weather the "TRUE" can do the last time actions, for example :

    next(a) := 
                 case 
                       a>0 : -10;
                       a<0 : 10;
                       TRUE : (do the last time actions);
                  esac;

In another word, when the 'a' = 0, if last time 'a' was assigned - 10, this time it will also be assigned - 10; if last time 'a' was assigned 10, this time it will also be assigned by 10.

So, now the question is that is it possible to do that by changing the source code of NuSMV, Could you tell me which is the c language file that implements the "TRUE" functions in "case"?

Thank you for your help!

Several approaches can be used.

Solution 1.

This solution is based on value persistence. Note that it can be used for the toy example you provided in your question, but it is by no means a general solution.

MODULE main
VAR
    a : -1..1;

ASSIGN
    init(a) := -1;
    next(a) := case
        a < 0 : 1;
        a > 0 : -1;
        TRUE  : a;
    esac;

Value persistence is sufficient because we are assigning a constant value to the variable.

Solution 2.

In case the value being assigned is not constant, value persistence cannot be used. Instead, we enrich the model with just enough memory so as to keep track of the actions being taken.

MODULE main
VAR
    a : -1..1;
    action : { ACTION_1, ACTION_2, NONE };

ASSIGN
    init(action) := NONE;
    next(action) := case
        a < 0 : ACTION_1;
        a > 0 : ACTION_2;
        TRUE  : action;
    esac;
    init(a) := -1;
    next(a) := case
        a < 0 : a + 1;
        a > 0 : a - 1;
        action = ACTION_1 : a + 1;
        action = ACTION_2 : a - 1;
        TRUE              : a;
    esac;

In this example action keeps track of the last choice that was performed on variable a. Whenever the preconditions of a's case are not sufficient to determine which action should be taken, we rely on our saved action value and replay the previously performed action.

Notice that it is the designer's responsibility to decide what should happen in the initial state in case none of the preconditions of a is triggered. In this case, we cannot replay a previous action (it doesn't exist), so the specification is open to being handled differently. In my case, I decided to let a stay on the value 0 forever.