I think this is getting unnecessarily complicated. The terms "extensional" and "intensional" in the answers above refer to a property of the language, not of sentences (yes your source does it, it can be done, but it's just complicating things here).
Simply put, an action is defined by the results it provides for particular instances of its primed and unprimed variables. That's it. There is no other property that matters. Two actions are the same if they provide the same results for the same "inputs" (instantiations of primed and unprimed variables). It doesn't matter how you express these actions, it doesn't matter if you gave them a name in a definition or what name you used, it doesn't matter if your computer takes longer to evaluate on action then the other.
So if you want two write two actions A and B that are different, then there has to be some pair of states (current state and next state) for which both actions provide a different result.
So for instance, if A and B represent actions by different servers, maybe you should have
A == some_formula /\ server' = "A"
B == some_formula /\ server' = "B"
Or perhaps more sensibly, maybe you want parametrisation over servers,
Action(s) == some_formula /\ server' = s
Not saying this necessarily is how you want to proceed. Just making it explicit that you need to model the difference you want to observe.
PS:
Regarding the generic concept of extensionality / intensionality. To talk about it you need to have some function like objects that can be applied to things, and what matters is if those objects are fully defined by the results of such applications, or if they have some other inherent properties that distinguish them.
This notion of "function like objects" that you apply to things, can show up in different "flavours".
- Usual function syntax. A function "f(x) = 2*(x+3)" is applied to "a" via "f(a)"
- Context holes. An expression with holes "C = 2* ( _ + 3)" can have its hole filled with "a" via "C[a]"
- Substitution. An expression "e = 2*x+3" can have its free variable substituted with "a" via a "e[x/a]"
In this discussion it's useful to think of the 3rd kind. The extensional nature of actions has to do with the results said actions return under specific "current state" and "next state". These states provide you with an instantiation via substitution of values for primed and unprimed variables.
I think this observation might be useful because I got the impression your answer seemed a bit confused by different notions of "application".
J.A.