chocosolver chokes on #property * a statement? #24

Closed
toeklk opened this Issue Dec 11, 2015 · 4 comments

Comments

Projects
None yet
3 participants
@toeklk

toeklk commented Dec 11, 2015

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

This comment has been minimized.

Show comment
Hide comment
@JLiangWaterloo

JLiangWaterloo Dec 11, 2015

Member

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 8af6d24).

Thanks for the bug report!

Member

JLiangWaterloo commented Dec 11, 2015

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 8af6d24).

Thanks for the bug report!

@JLiangWaterloo

This comment has been minimized.

Show comment
Hide comment
@JLiangWaterloo

JLiangWaterloo Dec 11, 2015

Member

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 a432d8d 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.
Member

JLiangWaterloo commented Dec 11, 2015

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 a432d8d 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

This comment has been minimized.

Show comment
Hide comment
@mantkiew

mantkiew Dec 11, 2015

Member

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.

Member

mantkiew commented Dec 11, 2015

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

This comment has been minimized.

Show comment
Hide comment
@toeklk

toeklk Dec 15, 2015

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!

toeklk commented Dec 15, 2015

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!

@mantkiew mantkiew referenced this issue Dec 23, 2015

Merged

Release 0.4.3 #26

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment