From d3d9a1aa8e1ad1a1e13b108b7f8273022b21f794 Mon Sep 17 00:00:00 2001
From: Yingjian Wang <yingjian.wang@mailbox.tu-dresden.de>
Date: Wed, 19 Jan 2022 00:24:44 +0100
Subject: [PATCH] Update Move.jadd
---
src/main/jastadd/hanoi/Move.jadd | 289 ++++++++++++++++---------------
1 file changed, 152 insertions(+), 137 deletions(-)
diff --git a/src/main/jastadd/hanoi/Move.jadd b/src/main/jastadd/hanoi/Move.jadd
index 86e03df..5e6430c 100644
--- a/src/main/jastadd/hanoi/Move.jadd
+++ b/src/main/jastadd/hanoi/Move.jadd
@@ -1,139 +1,154 @@
-import java.util.*;
-aspect Connectives{
- uncache Connective.eval();
- syn boolean Connective.eval();
- eq Conjunction.eval(){
- return this.getLeft().eval() && this.getRight().eval();
- }
- eq Disjunction.eval(){
- return this.getLeft().eval() || this.getRight().eval();
- }
- eq Implication.eval(){
- return (!this.getLeft().eval()) || this.getRight().eval();
- }
- eq Negation.eval()= !getConnective().eval();
- eq Atom.eval(){
- return this.getRelation().eval();
- }
- uncache Relation.eval();
- syn boolean Relation.eval();
- eq Subsetof.eval(){
- Set left=new HashSet<>();
- for(String element : this.getLeft().Set()){
- left.add(element);
- }
- Set right=new HashSet<>();
- for(String element : this.getRight().Set()){
- right.add(element);
- }
- return right.containsAll(left);
- }
- eq Compare.eval(){
- return (this.getLeft().eval() - this.getRight().eval())<0;
- }
- eq Equal.eval(){
- return this.getLeft().eval() - this.getRight().eval()==0;
- }
- uncache Term.eval();
- syn int Term.eval();
- eq Plus.eval(){
- return this.getLeft().eval() + this.getRight().eval();
- }
- eq Minus.eval(){
- return this.getLeft().eval() - this.getRight().eval();
- }
- eq Multi.eval(){
- return this.getLeft().eval() * this.getRight().eval();
- }
- eq Divide.eval(){
- return this.getLeft().eval() / this.getRight().eval();
- }
- eq Mod.eval(){
- return this.getLeft().eval() % this.getRight().eval();
- }
- eq IfThenElse.eval(){
- if(this.getIf().Satisfied()){
- return this.getThen().eval();
- }
- return this.getElse().eval();
- }
- eq CompareFunction.eval(){
- if(this.getLeft().eval() < this.getRight().eval()){
- return 1;
- }
- return 0;
- }
- eq EqualFunction.eval(){
- if(this.getLeft().eval() == this.getRight().eval()){
- return 1;
- }
- return 0;
- }
- eq SubsetofFunction.eval(){
- Set left=new HashSet<>();
- for(String element : this.getLeft().Set()){
- left.add(element);
- }
- Set right=new HashSet<>();
- for(String element : this.getRight().Set()){
- right.add(element);
- }
- if(right.containsAll(left)){
- return 1;
- }
- return 0;
- }
- eq ConstantNum.eval(){
- return this.getNum();
- }
- eq PillarID.eval(){
- return this.getRel().ID();
- }
- eq TotalDiskAmount.eval(){
- return this.getRel().AmountD();
- }
- eq DisksOnPillar.eval(){
- return this.getRel().getNumDisk();
- }
- eq TopDiskSize.eval(){
- return this.getRel().getDisk(this.getRel().getNumDisk()-1).getSize();
- }
-//customerized terms
- eq Term1.eval(){//return the size of top disk
- if(this.getRel().getNumDisk()>0){
- //if the pillar is not empty, check if the top disk has size 1
- return this.getRel().getDisk(this.getRel().getNumDisk()-1).getSize();
+aspect Move{
+ public boolean Constraint.oddTurnMove(Pillar P0, Pillar P1){
+ /*for every odd turn(turn==true), move the smallest disk D0 in sequence. |-----------Right:DisksOnPillar(P0)
+ Therefore, ValidTarget checks for a move from P0 to P1, when D0 is on the top of P0. |------If():ComparFunction()------Left:ConstantNumM0(0)
+ Conjunction()-------------hasSmallestDisk()---------R0()-----------------F0()----------------|------Then():P0TopDiskSize()
+ | TopDiskSizeEq1 IfThenElse |------Else():ConstantNumM1(-1)
+ | |
+ | |----------ConstantNum1(1)
+ |---ValidTarget()---------R1()---------P1.ID()
+ P1EqTarget
+ |
+ |-----Mod0()------Left:Plus0()------Left:Plus1()------Left:Mod1()------TotalDiskAmount();
+ | | | |------------ConstantNum2(2)
+ | | |--------ConstantNum1(1)
+ | |------P0.ID
+ |------ConstantNum3(3)*/
+ Conjunction ValidMove=new Conjunction();
+
+ Atom hasSmallestDisk=new Atom();//if the smallest disk is on this pillar
+ Equal TopDiskSizeEq1= new Equal();
+ IfThenElse TopDiskChecher=new IfThenElse();
+ CompareFunction PillarHasDisk=new CompareFunction();
+ TopDiskSize P0TopDiskSize=new TopDiskSize();
+ ConstantNum NumM1=new ConstantNum();
+ ConstantNum Num1=new ConstantNum();
+ ConstantNum Num0=new ConstantNum();
+ DisksOnPillar DisksOnP0=new DisksOnPillar();
+
+ Atom ValidTarget=new Atom();//check if the move sequence from P0 to P1 is valid
+ Equal P1EqTarget= new Equal();
+ PillarID P1ID=new PillarID();
+ Mod Mod0=new Mod();
+ Mod Mod1=new Mod();
+ Plus Plus0=new Plus();
+ Plus Plus1=new Plus();
+ TotalDiskAmount DisksOverall=new TotalDiskAmount();
+ PillarID P0ID=new PillarID();
+ ConstantNum Num2=new ConstantNum();
+ ConstantNum Num3=new ConstantNum();
+
+ ValidMove.setLeft(hasSmallestDisk);
+ ValidMove.setRight(ValidTarget);
+
+ NumM1.setNum(-1);
+ Num0.setNum(0);
+ Num1.setNum(1);
+ Num2.setNum(2);
+ Num3.setNum(3);
+
+ TopDiskSizeEq1.setLeft(TopDiskChecher);
+ TopDiskChecher.setIf(PillarHasDisk);
+ PillarHasDisk.setLeft(Num0);
+ PillarHasDisk.setRight(DisksOnP0);
+ DisksOnP0.setRel(P0);
+ TopDiskChecher.setThen(P0TopDiskSize);
+ P0TopDiskSize.setRel(P0);
+ TopDiskChecher.setElse(NumM1);
+ TopDiskSizeEq1.setRight(Num1);
+ hasSmallestDisk.setRelation(TopDiskSizeEq1);
+
+ ValidTarget.setRelation(P1EqTarget);
+ P1EqTarget.setLeft(P1ID);
+ P1ID.setRel(P1);
+ P1EqTarget.setRight(Mod0);
+ Mod0.setLeft(Plus0);
+ Mod0.setRight(Num3);
+ Plus0.setLeft(Plus1);
+ Plus0.setRight(P0ID);
+ P0ID.setRel(P0);
+ Plus1.setLeft(Mod1);
+ Plus1.setRight(Num1);
+ Mod1.setLeft(DisksOverall);
+ DisksOverall.setRel(P0);
+ Mod1.setRight(Num2);
+
+ this.addConnective(ValidMove);
+ if(this.getConnective(0).eval()){
+ System.out.println("Odd turn: P" + P0.ID() +".hahasSmallestDisk0 && (P" + P0.ID() +".target == P" + P1.ID()+")");
+ return true;//odd turn and valid move
}else{
- return -1;//no disk, the number is invalid, return -1
+ return false;
}
- }
- eq Term2.eval(){
- return this.getRel().moveSeq();
- }
- eq Term3.eval(){
- return this.getRel().ID();
- }
- uncache Condition.Satisfied();
- syn boolean Condition.Satisfied();
- eq CompareFunction.Satisfied(){
- return this.getLeft().eval() < this.getRight().eval();
- }
- eq EqualFunction.Satisfied(){
- return this.getLeft().eval() == this.getRight().eval();
- }
- eq SubsetofFunction.Satisfied(){
- Set left=new HashSet<>();
- for(String element : this.getLeft().Set()){
- left.add(element);
- }
- Set right=new HashSet<>();
- for(String element : this.getRight().Set()){
- right.add(element);
- }
- return right.containsAll(left);
- }
- public String[] Term.Set(){
- String[] str=new String[]{};
- return str;
- }
-}
+ }
+ public boolean Constraint.evenTurnMove(Pillar P0, Pillar P1){
+ /*for every even turn(turn==false), move the disk D on top of P0 to P1:
+ D is not D0(the smallest disk).
+ There is always one D can be moved in the even turn according to the game rules.
+ Statements:
+ 1.P0 is not empty: not OND().
+ 2.When condition 1 holds, P1 can be empty: TND().
+ 3.When 1 holds and 2 doesn’t hold, D0 < D1(for the disks on the top of P0 and P1 respectively).
+ Therefore, we want not OND() and (TND() or ValidTarget()) to be true.
+ |-----------hasSmallestDisk()-----------------R0---------------T0()
+ C1 |C3 |----------------T3()
+ Conjunction()-------------Negation()------Disjunction()----OND()----------------R1()----------------T0()
+ C0 | |----------------T2()
+ |---Disjunction()-----------TND()--------------R2()---------T1()
+ |C2 |-----------T2()
+ |------------------ValidTarget()-----------------R3()---------T0()
+ |---------T1*/
+ Conjunction C0=new Conjunction();
+ Negation C1=new Negation();
+ Disjunction C2=new Disjunction();
+ Disjunction C3=new Disjunction();
+ Atom hasSmallestDisk=new Atom();//if the smallest disk is on this pillar
+ Atom OND=new Atom();//origin has no disk
+ Atom TND=new Atom();//target has no disk
+ Atom ValidTarget=new Atom();//check the size, if the disk on the top of origin has smaller size than the one on target
+
+ C0.setLeft(C1);
+ C0.setRight(C2);
+ C1.setConnective(C3);
+ C2.setLeft(TND);
+ C2.setRight(ValidTarget);
+ C3.setLeft(hasSmallestDisk);
+ C3.setRight(OND);
+
+ Term1 T0=new Term1();//return size of top disk, return -1 when no disk.
+ Term1 T1=new Term1();
+ ConstantNum T2=new ConstantNum();
+ ConstantNum T3=new ConstantNum();
+
+ T0.setRel(P0);
+ T1.setRel(P1);
+ T2.setNum(0);
+ T3.setNum(1);
+
+ Equal R0=new Equal();
+ Compare R1=new Compare();
+ Compare R2=new Compare();
+ Compare R3=new Compare();
+
+ R0.setLeft(T0);
+ R0.setRight(T3);
+ R1.setLeft(T0);
+ R1.setRight(T2);
+ R2.setLeft(T1);
+ R2.setRight(T2);
+ R3.setLeft(T0);
+ R3.setRight(T1);
+ hasSmallestDisk.setRelation(R0);
+ OND.setRelation(R1);
+ TND.setRelation(R2);
+ ValidTarget.setRelation(R3);
+
+ this.addConnective(C0);
+ if(this.getConnective(0).eval()){
+ System.out.println("Even turn: !(P" + P0.ID() +".#disk == 0 || P" + P0.ID() +".hahasSmallestDisk0) && (P" + P1.ID() +".#disk == 0 || P" + P0.ID() +".topDisk < P" + P1.ID() +".topDisk)");
+ return true;//even turn and valid move
+ }
+ return false;
+ }
+ }
+
--
GitLab