chocosolver chokes on #property * a statement?

[toeklk]

Note: Resubmission of gsdlab/ClaferChocoIG#7. I just checked with 0.4.2.1 (binary distribution), and the problem is exactly the same. As it's friday evening, it's a perfect moment to do these kinds of things :-)

Consider the following clafer model

abstract Platform
    price -> int = sum hwComponents.price
    hwComponents -> HWComponent 1..2

abstract HWComponent
    price -> int

abstract Deployment
    price -> int = #platforms * 10 + sum platforms.price // causes chocosolver to choke?
    platforms : Platform 2..3

CAN : HWComponent
   [ price = 10 ]

DO : HWComponent
   [ price = 2 ]

D1: Deployment

// << min D1.price >>

Whereas claferIG seems to be able to succesfully generate instances from this model, it seems like the chocoIG fails to do the same. Removing the #platforms * 10 clause seems to "solve" the issue

[kgad@Klaass-MacBook-Air ~/Workspaces/varies/be.fmtc.costOptimization/Model]$  
 claferIG --maxint 64 ~/Workspaces/varies/be.fmtc.costOptimization/Model/NRE_test.cfr
=== Instance 1 Begin ===

CAN
  price$1 = 10
D1
  price$2 = 32
  platforms$1
    price$3 = 10
    hwComponents$1 = CAN
  platforms$2
    price$4 = 2
    hwComponents$2 = DO
DO
  price$5 = 2

--- Instance 1 End ---

claferIG> q
AlloyIG stream closed.
[kgad@Klaass-MacBook-Air ~/Workspaces/varies/be.fmtc.costOptimization/Model]$  
 java -jar ~/install/clafer/claferchocoig-0.3.9-jar-with-dependencies.jar -n 1 --minint 0 --maxint 64 --file NRE_test.cfr
Clafer Choco Instance Generator and Multi-Objective Optimizer
Compiling the Clafer model...
Running Model...

and then the the solver seems to get stuck in an endless loop...

Add-on questions from a follow-up comment on my side:

On the other hand, would there (in this particular case) be a possibility to somehow declare that the price attribute of the Deployment variable is "derived" (in the UML sense), such that the backend knows it should actually not branch on this variable for instance?

[JLiangWaterloo]

I'd forgotten about this issue.

It turns out the issue was actually due to the Fourier-Motzkin elimination optimization. Long story short, it was spinning in an infinite loop because it couldn't detect a fixed-point due to the way linear equations were being eliminated.

The problem is now fixed in the latest chocosolver develop branch (commit 8af6d2478c9138c76f63474de835c5bc18fa8e0c).

Thanks for the bug report!

[JLiangWaterloo]

On the other hand, would there (in this particular case) be a possibility to somehow declare that the price attribute of the Deployment variable is "derived" (in the UML sense), such that the backend knows it should actually not branch on this variable for instance?

I've added a feature in commit a432d8d6859be3f87a41db9e0a20e57b99b683a8 that can be used to have this same effect. The feature is very new, so you will have to do a bit of manual work to take advantage of it right now. For this specific example, you would add the following line to your .js file:

branchingPriority([[c0_hwComponents, c0_platforms, c0_CAN, c0_DO, c0_D1, c0_price, c1_price]]);

Couple of notes.

1. The two square brackets is not a typo.
2. Here, I am listing the Clafers that should have the highest priority for branching. Note that the price attribute of Deployment is "c2_price", which is not in the list above.
3. The Clafer names must correspond to the names in the .js file, which is slightly different than the names in the original Clafer model. This is why you see the c#_ prefixes.
4. The rest of the tool chain does not support this yet since it is very new.

[mantkiew]

You can use Choco escapes to add that piece directly into your Clafer model:

[choco|
branchingPriority([[c0_hwComponents, c0_platforms, c0_CAN, c0_DO, c0_D1, c0_price, c1_price]]);
|]

the contents of choco escapes are added at the end of the compiler's output for choco.

If a name is unique in the whole model, then it'll always have the c0_ prefix. But because two different clafers have the name price, we have c0_price, c1_price. The numbers are added based on occurence: c0_price is the first clafer price, c1_price, the second, and so on.

[toeklk]

Seriously, it's time for a new release :-)

[kgad@lt00858 ~/Workspaces/varies/be.fmtc.costOptimization/Model]$  
 time java -jar ~/install/clafer-tools-0.4.2.1/chocosolver.jar -n 1 --minint 0 --maxint 10000 --prettify --file ~/Workspaces/varies/be.fmtc.costOptimization/Model/deploymentModel_edited_scopes-3apps.js 
Optimizing...
=== Instance 1 Begin ===
[snip]
c0_D1$0
  c3_price$0 = 8800
--- Instance 1 End ---
Generated 1 optimal instance(s) within the scope

user    247m54.414s

[kgad@lt00858 ~/Workspaces/varies/be.fmtc.costOptimization/Model]$  
 time java -jar ~/git/gsdlab/chocosolver/target/chocosolver-0.4.3-jar-with-dependencies.jar -n 1 --minint 0 --maxint 10000 --prettify --file ~/Workspaces/varies/be.fmtc.costOptimization/Model/deploymentModel_edited_scopes-3apps_withBranchingStrategy.cfr
Compiling the Clafer model...
Optimizing...
=== Instance 1 Begin ===
[snip]
c0_D1$0
  c3_price$0 = 8800
--- Instance 1 End ---

Generated 1 optimal instance(s) within the scope

user    9m24.924s

Thx for this!