Require () on actions without parameters?

[konnov]

We have the special syntax for the parametereless definitions (val and pure val).

We do not have any special syntax for actions that have zero parameters. I have caught myself writing Init() and Next() in REPL multiple times instead of writing Init and Next. Perhaps, we should require actions to be applied via () only? IMO, this is consistent with the notion of an action.

If we do that, the next question is what to do about temporal formulas.

[shonfeder]

Shouldn't this be consistent across all operators, rather than just across actions?

[bugarela]

If we are dropping nullary opeators (as we talked about doing in https://github.com/informalsystems/quint/issues/881), then this doesn't make sense anymore, right?

[thpani]

If we are dropping nullary opeators (as we talked about doing in #881)

We still need nullary actions, no? (#881 was about nullary defs specifically, afaict)

[bugarela]

We still need nullary actions, no? (#881 was about nullary defs specifically, afaict)

I think all actions have to be nullary. #881 is about disallowing users to type () in definitions, which might lead them to think they have control over something being nullary or not - which they don't, as all defs and cals are non-nullary and all actions are nullary.

Also, this is all regarding the actual effect of the definition, and not the annotation, as one can write action x = 1 + 1 and that won't be nullary.

[konnov]

I think all actions have to be nullary

Actions do not have to be nullary. It's quite convenient to have actions like Deposit(fromAddr, toAddr, amount). It's actually up to us what to do about nullary actions. For instance, action step() = ... could indicate that it's not like a standard definition but a definition of an action, which is different from a value. Of course, in presence of the keyword action it seems to be redundant.

[bugarela]

I think all actions have to be nullary

I meant all actions without parameters have to be nullary. In the sense that is no difference between action foo = ... and action foo() = .... In practice, they will both be re-evaluated every time they are called.