The constrained output type in output variables with enum type

[verifierlife]

This file prompts: Error at line 5: 72 function main may not use constrained output type (subrange or enumeration) function main (choice: payload) returns (wolf, golds, cabbage, farmer: side);

Why it happens? Some solutions please.

---

--farmer2.lus type payload = enum { Empty, Wolf, Goat, Cabbage }; type side = enum { Left, Right };

function main(choice : payload) returns (wolf, goat, cabbage, farmer : side);

node testMain(choice : payload[2]) returns (wolf, goat, cabbage, farmer : side[2]); var wolf_0: side; wolf_1: side; golt_0: side; golt_1: side; cabbage_0: side; cabbage_1: side; farmer_0: side; farmer_1: side; let wolf_0, golt_0, cabbage_0, farmer_0 = main(choice[0]); wolf_1, golt_1, cabbage_1, farmer_1 = main(choice[1]); wolf = [wolf_0, wolf_1]; goat = [goat_0, goat_1]; cabbage = [cabbage_0, cabbage_1]; farmer = [farmer_0, farmer_1]; tel;

[agacek]

JKind (currently) doesn't allow functions to have constrained output types. I believe the reasoning is that a constrained output type means we would have to include assertions everywhere that function is used to ensure that the result value is within the constrained range.

You have two options:

1. You can use a node instead of a function, though this requires you to explicitly specify the behavior of the node.
2. You can return a type like int which requires you to have a way of converting that int into the constrained range.

Looking at your example, it's hard for me to tell what you are trying to accomplish with this function. I suspect that you want a node instead.