#536 miscounted parameters

[Kimmo Varpaaniemi]

This report concerns at least Rodin Platform 2.0.1 with Modularisation Plugin 1.4.3.201012161256.

In the attached Event-B project, the machine "kayttaja" has the events "evt_Alpha" and "evt_Beta" that are displayed below. The "corresponding" Rodin Problems messages are "Too few parameters in a call to Alpha; supplied 0, expected 2" and "Too many parameters in a call to Beta; supplied 3, expected 2". Actually, the number of supplied parameters is 2 in both cases. It seems that I should no longer rely on the parser.

evt_Alpha ≙
STATUS
ordinary
ANY
a
WHERE
grd_a : a ∈ ℤ → (ℤ → ℤ)
THEN
act_y : y ≔ Alpha(a(1)(2) ↦ 3)
END

evt_Beta ≙
STATUS
ordinary
ANY
b
WHERE
grd_b : b ∈ ℤ → ((ℤ × ℤ × ℤ) → ℤ)
THEN
act_y : y ≔ Beta(b(4)(5 ↦ 6 ↦ 7) ↦ 8)
END

[Kimmo Varpaaniemi]

[Alex Iliasov]

There are no warning or errors for this project in the current build.

[Kimmo Varpaaniemi]

The original bug description applies to Rodin Platform 2.2.1 with Modularisation Plugin 1.4.3.201102120042.

[Kimmo Varpaaniemi]

I am not happy with the fix. Rodin Platform 2.2.2 with Modularisation Plugin 2.2.1.201108011025 produces kayttaja.bcm where calls to the operations Alpha and Beta are "passed through".

<org.eventb.core.scEvent name="liittyma_operationv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt_Alpha" org.eventb.core.source="/ParameterCountingTest/kayttaja.bum|org.eventb.core.machineFile#kayttaja|org.eventb.core.event#0">
<org.eventb.core.scParameter name="a" org.eventb.core.source="/ParameterCountingTest/kayttaja.bum|org.eventb.core.machineFile#kayttaja|org.eventb.core.event#0|org.eventb.core.parameter#'" org.eventb.core.type="ℙ(ℤ×ℙ(ℤ×ℤ))"/>
<org.eventb.core.scGuard name="grd0" org.eventb.core.label="grd_a" org.eventb.core.predicate="a∈ℤ → (ℤ → ℤ)" org.eventb.core.source="/ParameterCountingTest/kayttaja.bum|org.eventb.core.machineFile#kayttaja|org.eventb.core.event#0|org.eventb.core.guard#grd0"/>
<org.eventb.core.scAction name="act0" org.eventb.core.assignment="y ≔ Alpha(a(1)(2) ↦ 3)" org.eventb.core.label="act_y" org.eventb.core.source="/ParameterCountingTest/kayttaja.bum|org.eventb.core.machineFile#kayttaja|org.eventb.core.event#0|org.eventb.core.action#act0"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="liittyma_operationw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="evt_Beta" org.eventb.core.source="/ParameterCountingTest/kayttaja.bum|org.eventb.core.machineFile#kayttaja|org.eventb.core.event#\/">
<org.eventb.core.scParameter name="b" org.eventb.core.source="/ParameterCountingTest/kayttaja.bum|org.eventb.core.machineFile#kayttaja|org.eventb.core.event#\/|org.eventb.core.parameter#(" org.eventb.core.type="ℙ(ℤ×ℙ(ℤ×ℤ×ℤ×ℤ))"/>
<org.eventb.core.scGuard name="grd0" org.eventb.core.label="grd_b" org.eventb.core.predicate="b∈ℤ → (ℤ × ℤ × ℤ → ℤ)" org.eventb.core.source="/ParameterCountingTest/kayttaja.bum|org.eventb.core.machineFile#kayttaja|org.eventb.core.event#\/|org.eventb.core.guard#grd0"/>
<org.eventb.core.scAction name="act0" org.eventb.core.assignment="y ≔ Beta(b(4)(5 ↦ 6 ↦ 7) ↦ 8)" org.eventb.core.label="act_y" org.eventb.core.source="/ParameterCountingTest/kayttaja.bum|org.eventb.core.machineFile#kayttaja|org.eventb.core.event#\/|org.eventb.core.action#act0"/>
</org.eventb.core.scEvent>

[Kimmo Varpaaniemi]

Rodin Platform 2.2.2 with Modularisation Plugin 2.2.1.201108221524 behaves as expected.