module testopen util/ordering[Natural] as ord

abstract sig Natural{}

one sig One extends Natural{}

one sig Two extends Natural{}

one sig Three extends Natural{}

one sig Four extends Natural{}

abstract sig Symbol{}

one sig Cross extends Symbol{}{}

one sig Fi extends Symbol{}{}

one sig Blade extends Symbol{}{}

one sig Star extends Symbol{}{}

sig Cell{

symbol: one Symbol,

rowIndex: Natural,

columnIndex: Natural,

inRange: Natural

}

fact Numbers{

ord/first() = One

ord/next(One) = Two

ord/next(Two) = Three

ord/last() = Four

}

pred defineRange(row:Natural,column:Natural,r:Natural){

all c:Cell |

c.rowIndex = row && c.columnIndex = column => c.inRange = r

}

fact DefineRange{

defineRange(One,One,Two)

defineRange(One,Two,One)

defineRange(One,Three,One)

defineRange(One,Four,One)

defineRange(Two,One,Two)

defineRange(Two,Two,Two)

defineRange(Two,Three,Three)

defineRange(Two,Four,One)

defineRange(Three,One,Four)

defineRange(Three,Two,Two)

defineRange(Three,Three,Three)

defineRange(Three,Four,Three)

defineRange(Four,One,Four)

defineRange(Four,Two,Four)

defineRange(Four,Three,Four)

defineRange(Four,Four,Three)

}

pred staticSymbols(row:Natural, column:Natural, s:Symbol){

all c:Cell |

c.rowIndex = row && c.columnIndex = column =>

c.symbol = s

}

fact{

staticSymbols(One,Four,Fi) &&

staticSymbols(Two,Two,Cross) &&

staticSymbols(Four,Two,Blade) &&

staticSymbols(Four,Three,Star)

}

// No two same symbols in the same Range

fact{

all disj c,c’:Cell |

c.inRange = c’.inRange =>

c.symbol != c’.symbol

}

// All cells have different rowIndex and columnIndex

fact{

no disj c,c’:Cell | (c.rowIndex = c’.rowIndex && c.columnIndex = c’.columnIndex)

}

//No two same symbols in the same row Column

fact{

all disj c,c’:Cell |

c.rowIndex = c’.rowIndex =>

c.symbol != c’.symbol

all disj c,c’:Cell |

c.columnIndex = c’.columnIndex =>

c.symbol != c’.symbol

}

pred solution(){

#Cell = 16

}

run solution for 16 Cell