ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืืื ืื ืืืขืจืึทืคืึทืงืืืฉืึทื ืคืื ืืืื ืคึผืจืึธืืจืึทื ืึธืืขืจ ืึทืืืขืจืืืึทื ื ืืฆื ืื ืืขืจื.
ืืึธืก ืืื ืืืื ืขืจ ืคืื ืื ืืขืจืกื ืฉืืึทืจืง ืืขืืืึธืืก ืึทื ืึทืืึทืื ืืืจ ืฆื ืืขืคึฟืื ืขื ืึทืืข ืืืึทืื ืขืจืึทืืืืืืื ืืื ืึท ืคึผืจืึธืืจืึทื ืึธืืขืจ ืืึทืืืืึทืื ืึทื ืืื ืืึธื ื ืื ืขืงืกืืกืืืจื.
ื ืืขืจ ืืืืืืื ืืึทืฉืจืืึทืืื ื ืคืื ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืงืขื ืขื ืืืื ืืขืืขื ืืื ืืขื ืืืึทืฉืคึผืื ืคืื ืกืึทืืืืื ื ืื ืคึผืจืึธืืืขื ืคืื ืืื ืืืื ืคืจืืขืจืืืงื ืึทืจืืืงื.
ืืื ืืขื ืึทืจืืืงื ืืื ืืึทื ืคืื ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืคืื ืคึผืจืึธืืืขืืก ืฆื ืืืืื ืืื ืืึทืฉืจืืึทืื ืืื
ืืื ืงืขื ืขื ืืื ืืืืืึธืืึทืืืฉ ืงืึธื ืืืขืจืืขื ืืื ืคืึธืจืืึทื ืืขืจืฉื ืกืืกืืขืืขื.
ืฆื ืืึธื ืืึธืก, ืืื ืืขืฉืจืืื ืืืื ืืืืืขื ืข ืึทื ืึทืืึธื ืคืื ืึท ืืืืจืืืึทื ืืึทืฉืื ืืื ืกืืืืึธืืืฉ ืคึผืจืื ืกืึทืคึผืึทืื.
ืขืก ืคึผืึทืจืกืื ืื ืคึผืจืึธืืจืึทื ืงืึธื ืืื ืืจืึทื ืกืืืืฅ ืขืก ืืื ืึท ืกืืกืืขื ืคืื ืืงืืืืืืฉืึทื ื (SMT), ืืืึธืก ืงืขื ืขื ืฉืืื ืืืื ืกืึทืืืื ืคึผืจืึธืืจืึทืืืึทืืืงืึทืืื.
ืืื ื ืืื ืคึฟืึธืจืืึทืฆืืข ืืืขืื ืกืืืืึธืืืฉ ืืฉืืื ืืช ืืื ืืขืจืืื ืื ืืืืฃ ืื ืืื ืืขืจื ืขื ืืึทื ืฅ ืคืจืึทืืืึทื ืืขืจืึทืื,
ืืื ืืืขื ืืขืงืืฆืขืจ ืืืฉืจืืืื ืืืืก ืขืก ืืื.
ืกืืืืึธืืืฉ ืงืึทืืคึผืืึทืืืืฉืึทื ืืื ืึท ืืืขื ืฆื ืกืืืืึทืืืืื ืืึทืกืื ืืืกืคืืจื ืึท ืคึผืจืึธืืจืึทื ืืืืฃ ืึท ืืจืืื ืงืืื ืคืื ืืึทืื ืืื ืืื ืื ืืืืคึผื ืืขืฆืืึทื ืคึฟืึทืจ ืคืึธืจืืึทื ืคึผืจืึธืืจืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื.
ืคึฟืึทืจ ืืืึทืฉืคึผืื, ืืืจ ืงืขื ืขื ืฉืืขืื ืึทืจืืึทื ืฉืจืืึทื ืื ืึธืื ืืื ืืขืจ ืขืจืฉืืขืจ ืึทืจืืืืขื ื ืงืขื ืขื ื ืขืืขื ืงืืื positive ืืืึทืืืขืก, ืื ืจืืข ื ืขืืึทืืืื, ืื ืืจืื ื ืื, ืืื ืืขืจ ืจืขืืืืืึทื ืึทืจืืืืขื ื, ืคึฟืึทืจ ืืืึทืฉืคึผืื, 42.
ืกืืืืึธืืืฉ ืืฉืืื ืืช ืืื ืืืื ืืืืคื ืืืขื ืืขืื ืืื ืื ืื ืขื ืืคืขืจ ืฆื ืฆื ืขืก ืืื ืืขืืืขื ืคึฟืึทืจ ืืื ืื ืฆื ืืึทืงืืืขื ืื ืืขืืืืื ืจืขืืืืืึทื ืืื ืึท ืืืึทืฉืคึผืื ืคืื ืึท ืกืืื ืคืื ืึทืืึท ืึทืจืืึทื ืฉืจืืึทื ืคึผืึทืจืึทืืขืืขืจืก. ืึธืืขืจ ืืขืจืืืืึทื ืึทื ืขืก ืืขื ืขื ื ืื ืึทืืึท ืคึผืึทืจืึทืืขืืขืจืก.
ืืขืจืฆื, ืืืจ ืงืขื ืขื ืฉืืขืื ืื ืึทืจืืึทื ืฉืจืืึทื ืึทืจืืืืขื ืื ืฆื ืึทืืข ืืขืืืขื ืึธื ืขืก, ืืื ืกืขืืขืงืืืจื ืืืืื ืื ืจืขืืืืืึทื ืึธื ืขืก, ืืืฉื, ืื ืึทืืืื ืืกืืจืึทืืึธืจ ืคึผืึทืจืึธื.
ืืื ืืขื ืคืึทื, ืืืจ ืืืขืื ืืขืคึฟืื ืขื ืึทืืข ืื ืืืึทืื ืขืจืึทืืืืืืื ืคืื ืื ืคึผืจืึธืืจืึทื ืึธืืขืจ ืืึทืงืืืขื ืืขืจืืืืึทื ืึทื ืืขืจ ืึทืืืื ืืกืืจืึทืืึธืจ ืก ืคึผืึทืจืึธื ืืื ืืืืขืจ.
ืขืก ืงืขื ืขื ืืืื ืื ืืขืืืืื ืึทื ืื ืงืืึทืกืืฉ ืืืจืืคืืจืื ื ืคืื ืึท ืคึผืจืึธืืจืึทื ืืื ืกืคึผืขืฆืืคืืฉ ืึทืจืืึทื ืฉืจืืึทื ืืึทืื ืืื ืึท ืกืคึผืขืฆืืขื ืคืึทื ืคืื ืกืืืืึธืืืฉ ืืืจืืคืืจืื ื.
ืืขืจืืืขืจ, ืืืื ืืึทืจืึทืงืืขืจ VM ืงืขื ืขื ืืืื ืึทืจืืขืื ืืื ืขืืืึทืืืืฉืึทื ืืึธืืข ืคืื โโืึท ื ืึธืจืืึทื ืืืืจืืืึทื ืืึทืฉืื.
ืืื ืื ืืึทืืขืจืงืื ืืขื ืฆื ืื ืคืจืืขืจืืืงืข ืึทืจืืืงื ืืืจ ืงืขื ืขื ืืขืคึฟืื ืขื ืึท ืฉืืื ืงืจืืืืง ืคืื ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืืื ืึท ืืืกืงืืกืืข ืคืื โโืืืึทื ืืืืงื ืึทืกืึทื.
ืื ืืืืคื ืคืจืืืืขืืขื ืืขื ืขื:
- ืงืึธืืืื ืึทืืึธืจืืึทื ืืงืกืคึผืืึธืืืฉืึทื, ืืื ื ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืืขืกืึธืฃ ืงืืื ืึทืจืึธืคึผ ืฆื ืคึผ = ื ืคึผ
- ืคึผืจืึทืกืขืกืื ื ืงืึทืืืก ืฆื ืื ืืขืงืข ืกืืกืืขื, ื ืขืืืืึธืจืงืก ืืื ืื ืืขืจืข ืคืื ืืจืืืกื ืืืง ืกืืึธืจืืืืฉ ืืื ืืขืจ ืฉืืืขืจ ืฆื ืืึทืฉืืขืืืงื
- ืืึทืื ืืื ืื ืกืคึผืขืกืืคืืงืึทืืืึธื, ืืืขื ืืขืจ ืงืื ื ืึธืืขืจ ืคึผืจืึธืืจืึทืืืกื ืืืขื ืืืื ืืึทื, ืึธืืขืจ ืืื ื ืืฉื ืืืกืงืจืืืื ืขืก ืึทืงืืขืจืึทืืื ืืขื ืื ืืื ืื ืืขืื ืืฉ ืกืคึผืขืกืึทืคืึทืงืืืฉืึทื ื.
ืืื ืึท ืจืขืืืืืึทื, ืื ืคึผืจืึธืืจืึทื ืืืขื ืืืื ืืืขืจืึทืคืืื ืืื ื ืึธืืงืืืขื ืืื ืื ืกืคึผืขืกืึทืคืึทืงืืืฉืึทื ื, ืึธืืขืจ ืืืขื ืืึธื ืขืคึผืขืก ืืึธืจ ืึทื ืืขืจืฉ ืคืื ืืืึธืก ืื ืงืจืืืืืขืจื ืืขืจืืืึทืจื ืคืื ืืื.
ืืื ื ืืื ืืขื ืึทืจืืืงื ืืื ืืื ืืขืจ ืืืืคึผื ืงืึทื ืกืืืขืจืื ื ืื ื ืืฆื ืคืื ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืืื ืคืืจ, ืืื ืืืขื ื ืืฉื ืงืืึทืคึผ ืืืื ืงืึธืคึผ ืงืขืื ืื ืืืึทื ื ืคึฟืึทืจ ืืืฆื, ืืื ืืืขื ืงืืืึทืื ืึท ืกืืกืืขื ืืื ืื ืึทืืืขืจืืืืืง ืงืึทืืคึผืืขืงืกืืื ืืื ืื ื ืืืขืจ ืคืื ืคืื ืืจืืืกื ืืืง ืจืืคื ืืขื ืขื ืืื ืืืึทื.
ืืื ื ืงืืื ืงืึทื ืืจืึทืงืฅ ืืขืกืืขืจ ืคึผืึทืกื ืื ืจืขืงืืืืจืขืืขื ืฅ, ืื ืืจืืจื ืืื ืืขืคืืื ืืืืฃ RIDE ืงืึทื ืืจืึทืงืฅ ืคืื ืื ืืืึทืืืขืก ืคึผืืึทืืคืึธืจืืข: ืืื ืืขื ืขื ื ืืฉื ืืืจืื ื ืืึทื ืฅ, ืืื ืืืืขืจ ืืึทืงืกืืืื ืงืึทืืคึผืืขืงืกืืื ืืื ืึทืจืืึทืคืืฉืึทืื ืืืืืืขื.
ืืืขืจ ืืืจ ืืืขืื ืืึทืืจืึทืืื ืืื ืืืืกืฉืืืกืืขื ืคืื ืื ืืขืื ืืฉ ืืืึทื.
ืืื ืึทืืืฉืึทื ืฆื ืึทืืฅ, ืคืึธืจืืึทื ืืืขืจืึทืคืึทืงืืืฉืึทื ืืืขื ืืืื ืกืคึผืขืฆืืขื ืืื ืคืึธืืขืจืื ื ืคึฟืึทืจ ืงืืื ืงืึทื ืืจืึทืงืฅ: ืขืก ืืื ืืืืฉืึทืืืึทืื ืืืืืขืืืขื ืฆื ืคืึทืจืจืืืื ืึท ืงืึธื ืืจืึทืงื ืืขืืช ื ืึธื ืขืก ืืื ืืึธื ืืฉื.
ืืื ืื ืคึผืจืืึทื ืคืื ืึทืืึท ืขืจืจืึธืจืก ืงืขื ืขื ืืืื ืืืืขืจ ืืืื, ืืืืึทื ืืึทื ืฅ ืืจืืืก ืึทืืึทืื ืฅ ืคืื ืืขืื ืืขื ืขื ืึธืคื ืกืืึธืจื ืืืืฃ ืงืืื ืงืึทื ืืจืึทืงืฅ.
ืืืึทื ืกืืืืึธืืืฉ ืืืืจืืืึทื ืืึทืฉืื ืืื ืืขืฉืจืืื ืืื PHP ืืื Python, ืืื ื ืืฆื Z3Prover ืคึฟืื Microsoft Research ืฆื ืกืึธืืืืข ืื ืจืืืึทืืืื ื ืกืื ืคืึธืจืืืืึทืก.
ืืื ืืืึทื ืืึทืจืฅ ืืื ืึท ืฉืืึทืจืง ืืึทืืื-ืืจืึทื ืกืึทืงืฉืึทื ืึทื ืืืื, ืืืึธืก
ืึทืืึทืื ืืืจ ืฆื ืืขืคึฟืื ืขื ืกืึทืืืฉืึทื ื ืึธืืขืจ ืืืึทืื ืขืจืึทืืืืืืื, ืืคืืื ืืืื ืขืก ืจืืงืืืืืขืจื ืคืืืข ืืจืึทื ืืึทืงืฉืึทื ื.
ืืคืืื , ืืืื ืขืจ ืคืื ืื ืืขืจืกื ืฉืืึทืจืง ืกืืืืึธืืืฉ ืคืจืึทืืขืืืึธืจืงืก ืคึฟืึทืจ ืืขืจืืืืื ื ืขืืืขืจืขืื ืืืึทืื ืขืจืึทืืืืืืื, ืืืืื ืฆืืืขืืขืื ืืขื ืคืืืืงืืื ืึท ืืืกื ืืืฉืื ืฆืืจืืง.
ืืืขืจ ืขืก ืืื ืืืื ืฆื ืืืืขืจืงื ืึทื ืืืขืจ ืงืึทื ืืจืึทืงืฅ ืืขื ืขื ืืขืจ ืงืึธืืคึผืืืฆืืจื ืืื ืืืจืื ื ืืึทื ืฅ.
PHP ืืจืึทื ืกืืืืฅ ืื ืืงืืจ ืงืึธื ืคืื ืื RIDE ืงืืื ืงืึธื ืืจืึทืงื ืืื ืึท ืคึผืืืืึธื ืฉืจืืคื, ืืื ืืืึธืก ืื ืคึผืจืึธืืจืึทื ืืื ืืขืจืืื ืื ืืื ืึท Z3 SMT-ืงืึทืืคึผืึทืืึทืืึทื ืกืืกืืขื ืคืื ืงืึธื ืืจืึทืงื ืฉืืึทืื ืืื ืื ืึธืื ืคึฟืึทืจ ืืืืขืจ ืืจืึทื ืืืฉืึทื ื:
ืืืฆื ืืื ืืืขื ืืึทืฉืจืืึทืื ืืืึธืก ืืื ืืขืฉืขืขื ืืฉ ืืื ืขืืืืื ืืง ืืื ืืขืจ ืืขืืึทื.
ืึธืืขืจ ืขืจืฉืืขืจ, ืึท ืืืกื ืืืขืจืืขืจ ืืืขืื ืื RIDE ืงืืื ืงืึธื ืืจืึทืงื ืฉืคึผืจืึทื.
ืขืก ืืื ืึท ืคืึทื ืืงืฉืึทื ืึทื ืืื ืืืืกืืจืืง-ืืืืืจื ืคึผืจืึธืืจืึทืืืื ื ืฉืคึผืจืึทื ืืืึธืก ืืื ืคืืื ืืืจื ืคึผืืึทื.
RIDE ืืืืคื ืืื ืืคืืขืืื ืืขืจืืงืืื ืืื ืื ืืืึทืงืืืืืืึทื ืืื ืงืขื ืขื ืฆืืจืืงืงืจืืื ืืื ืฉืจืืึทืื ืืื ืคึฟืึธืจืืึทืฆืืข ืคึฟืื ืกืืึธืจืืืืฉ ืืื ืืงื ืฆื ืืขืจ ืืึทื ืืฆืขืจ ืก ืืืึทืื.
ืืืจ ืงืขื ืขื ืฆืืืฉืขืคึผืขื ืึท RIDE ืงืึธื ืืจืึทืงื ืฆื ืืขืืขืจ ืืืึทืื, ืืื ืืขืจ ืจืขืืืืืึทื ืคืื ืืืจืืคืืจืื ื ืืืขื ืืืื ืืืืื ืืืช ืึธืืขืจ ืคืึทืืฉ.
TRUE ืืืื ืึทื ืืขืจ ืงืืื ืงืึธื ืืจืึทืงื ืึทืืึทืื ืื ืืจืึทื ืกืึทืงืืืึธื, ืืื FALSE ืืืื ืึทื ืขืก ืคึผืจืึธืืืืืึทืฅ ืขืก.
ื ืคึผืฉืื ืืืึทืฉืคึผืื: ืึท ืฉืจืืคื ืงืขื ืขื ืคืึทืจืืืขืจื ืึท ืึทืจืืืขืจืคืืจื ืืืื ืื ืืืึทืื ืืืึธื ืืื ืืืืื ืืงืขืจ ืืื 100.
ืืื ืึท ืืืึทืฉืคึผืื, ืืื ืืืขื ื ืขืืขื ืื ืืขืืืข ืืืืืฃ, ืฆืื ืืื ืงืจืืื, ืึธืืขืจ ืฉืืื ืืขืจืืื ืื ืืื ืื ืคืึธืจืขื ืคืื ืึท ืงืืื ืงืึธื ืืจืึทืงื.
ืืขืจ ืืื ืืฆืขืจ ืืืขื ื ืืฉื ืงืขื ืขื ืืจืืืกืฆืืขื ืืขืื ืคืื ืื ืืืืื ืืืืฃ ืืืขืืื ืืขืจ ืงืื ืืจืืงื ืืื ืืจืืืกืืขืฉืืขืื ืืขืืืืจื ืืื ืขืจ ืืื ืืืขืืขื ืืขืฉืืงื ืืืืฃ ืืขืจ ืื ืืขืจืขืจ ืืืื.
#ะะทะฒะปะตะบะฐะตะผ ะฟะพะปะพะถะตะฝะธะต ะฒัะตั
ะพะฑัะตะบัะพะฒ ะธะท ะฑะปะพะบัะตะนะฝะฐ
let contract = tx.sender
let human= extract(getInteger(contract,"human"))
let wolf= extract(getInteger(contract,"wolf"))
let goat= extract(getInteger(contract,"goat"))
let cabbage= extract(getInteger(contract,"cabbage"))
#ะญัะพ ัะฐะบ ะฝะฐะทัะฒะฐะตะผะฐั ะดะฐัะฐ-ััะฐะฝะทะฐะบัะธั, ะฒ ะบะพัะพัะพะน ะฟะพะปัะทะพะฒะฐัะตะปั ะฟัะธััะปะฐะตั ะฝะพะฒัะต 4 ะฟะตัะตะผะตะฝะฝัะต.
#ะะพะฝััะฐะบั ัะฐะทัะตัะธั ะตั ัะพะปัะบะพ ะฒ ัะปััะฐะต ะตัะปะธ ะฒัะต ะพะฑัะตะบัั ะพััะฐะฝัััั ะฒ ัะพั
ัะฐะฝะฝะพััะธ.
match tx {
case t:DataTransaction =>
#ะะทะฒะปะตะบะฐะตะผ ะฑัะดััะตะต ะฟะพะปะพะถะตะฝะธะต ะฒัะตั
ะพะฑัะตะบัะพะฒ ะธะท ััะฐะฝะทะฐะบัะธะธ
let newHuman= extract(getInteger(t.data,"human"))
let newWolf= extract(getInteger(t.data,"wolf"))
let newGoat= extract(getInteger(t.data,"goat"))
let newCabbage= extract(getInteger(t.data,"cabbage"))
#0 ะพะฑะพะทะฝะฐัะฐะตั, ััะพ ะพะฑัะตะบั ะฝะฐ ะปะตะฒะพะผ ะฑะตัะตะณั, ะฐ 1 ััะพ ะฝะฐ ะฟัะฐะฒะพะผ
let humanSide= human == 0 || human == 1
let wolfSide= wolf == 0 || wolf == 1
let goatSide= goat == 0 || goat == 1
let cabbageSide= cabbage == 0 || cabbage == 1
let side= humanSide && wolfSide && goatSide && cabbageSide
#ะัะดัั ัะฐะทัะตัะตะฝั ัะพะปัะบะพ ัะต ััะฐะฝะทะฐะบัะธะธ, ะณะดะต ั ะบะพะทะพะน ะฝะธะบะพะณะพ ะฝะตั ะฒ ะพััััััะฒะธะธ ัะตัะผะตัะฐ.
let safeAlone= newGoat != newWolf && newGoat != newCabbage
let safe= safeAlone || newGoat == newHuman
let humanTravel= human != newHuman
#ะกะฟะพัะพะฑั ะฟััะตัะตััะฒะธั ัะตัะผะตัะฐ ััะดะฐ ะธ ะพะฑัะฐัะฝะพ, ั ะบะตะผ-ัะพ ะปะธะฑะพ ะฒ ะพะดะธะฝะพัะบั.
let t1= humanTravel && newWolf == wolf + 1 && newGoat == goat && newCabbage == cabbage
let t2= humanTravel && newWolf == wolf && newGoat == goat + 1 && newCabbage == cabbage
let t3= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage + 1
let t4= humanTravel && newWolf == wolf - 1 && newGoat == goat && newCabbage == cabbage
let t5= humanTravel && newWolf == wolf && newGoat == goat - 1 && newCabbage == cabbage
let t6= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage - 1
let t7= humanTravel && newWolf == wolf && newGoat == goat && newCabbage == cabbage
let objectTravel = t1 || t2 || t3 || t4 || t5 || t6 || t7
#ะะพัะปะตะดะฝัั ัััะพะบะฐ ะฒ ัะฐะทะดะตะปะต ััะฐะฝะทะฐะบัะธะธ ะพะฟะธััะฒะฐะตั ัะฐะทัะตัะฐััะตะต ััะฐะฝะทะฐะบัะธั ััะปะพะฒะธะต.
#ะะตัะตะผะตะฝะฝัะต ััะฐะฝะทะฐะบัะธะธ ะดะพะปะถะฝั ะธะผะตัั ะทะฝะฐัะตะฝะธั 1 ะธะปะธ 0, ะฒัะต ะพะฑัะตะบัั ะดะพะปะถะฝั
#ะฑััั ะฒ ะฑะตะทะพะฟะฐัะฝะพััะธ, ะฐ ัะตัะผะตั ะดะพะปะถะตะฝ ะฟะตัะตะฟะปัะฒะฐัั ัะตะบั ะฒ ะพะดะธะฝะพัะบั
#ะธะปะธ ั ะบะตะผ-ัะพ ะฝะฐ ะบะฐะถะดะพะผ ัะฐะณั
side && safe && humanTravel && objectTravel
case s:TransferTransaction =>
#ะขัะฐะฝะทะฐะบัะธั ะฒัะฒะพะดะฐ ััะตะดััะฒ ัะฐะทัะตัะตะฝะฐ ัะพะปัะบะพ ะฒ ัะปััะฐะต ะตัะปะธ ะฒัะต ะฟะตัะตะฟะปัะปะธ ะฝะฐ ะดััะณะพะน ะฑะตัะตะณ
human == 1 && wolf == 1 && goat == 1 && cabbage == 1
#ะัะต ะฟัะพัะธะต ัะธะฟั ััะฐะฝะทะฐะบัะธะน ะทะฐะฟัะตัะตะฝั
case _ => false
}
PHP ืขืจืฉืืขืจ ืขืงืกืืจืึทืงื ืึทืืข ืืืขืจืืึทืืึทืื ืคืื ืื ืงืืื ืงืึธื ืืจืึทืงื ืืื ืื ืคืึธืจืขื ืคืื ืืืืขืจ ืฉืืืกืืขื ืืื ืื ืงืึธืจืึทืกืคึผืึทื ืืื ื ืืึธืึธืืขืึทื ืืืืกืืจืืง ืืืึทืืขืืืืืง.
cabbage: extract ( getInteger ( contract , "cabbage" ) )
goat: extract ( getInteger ( contract , "goat" ) )
human: extract ( getInteger ( contract , "human" ) )
wolf: extract ( getInteger ( contract , "wolf" ) )
fState: human== 1 && wolf== 1 && goat== 1 && cabbage== 1
fState:
wolf:
goat:
cabbage:
cabbageSide: cabbage== 0 || cabbage== 1
human: extract ( getInteger ( contract , "human" ) )
newGoat: extract ( getInteger ( t.data , "goat" ) )
newHuman: extract ( getInteger ( t.data , "human" ) )
goatSide: goat== 0 || goat== 1
humanSide: human== 0 || human== 1
t7: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage
t3: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage + 1
t6: humanTravel && newWolf== wolf && newGoat== goat && newCabbage== cabbage - 1
t2: humanTravel && newWolf== wolf && newGoat== goat + 1 && newCabbage== cabbage
t5: humanTravel && newWolf== wolf && newGoat== goat - 1 && newCabbage== cabbage
t1: humanTravel && newWolf== wolf + 1 && newGoat== goat && newCabbage== cabbage
t4: humanTravel && newWolf== wolf - 1 && newGoat== goat && newCabbage== cabbage
safeAlone: newGoat != newWolf && newGoat != newCabbage
wolfSide: wolf== 0 || wolf== 1
humanTravel: human != newHuman
side: humanSide && wolfSide && goatSide && cabbageSide
safe: safeAlone || newGoat== newHuman
objectTravel: t1 || t2 || t3 || t4 || t5 || t6 || t7
PHP ืืขืืึธืื ืงืึทื ืืืขืจืฅ ืืื ืืื ืึท Z3Prover SMT-ืงืึทืืคึผืึทืืึทืืึทื ืกืืกืืขื ืืึทืฉืจืืึทืืื ื ืืื ืคึผืืืืึธื.
ืื ืืึทืื ืืขื ืขื ืืื ืืขืืืืงืื ืืื ืึท ืฉืืืืฃ, ืืื ืกืืึธืจืืืืฉ ืืืขืจืืึทืืึทืื ืืึทืงืืืขื ืืื ืืขืงืก ืืื, ืืจืึทื ืกืึทืงืืืึธื ืืืขืจืืึทืืึทืื ืืื ืืขืงืก i + 1, ืืื ืืืขืจืืึทืืึทืื ืืื ืืืืกืืจืืงื ืฉืืขืื ืื ืึผืืืื ืคึฟืึทืจ ืืืขืจืืึทื ื ืคืื ืื ืคืจืืขืจืืืงืข ืฉืืึทื ืฆื ืืขืจ ืืืืึทืืขืจ.
ืืึธืก ืืื ืื ืืึทืจืฅ ืคืื ืืื ืืืขืจ ืืืืจืืืึทื ืืึทืฉืื, ืืืึธืก ืืื ืึท ืืึทืืื-ืืจืึทื ืกืึทืงืฉืึทื ืึทื ืืืื ืืขืงืึทื ืืืึทื.
fState: And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 )
final: fState[Steps]
fState:
wolf:
goat:
cabbage:
cabbageSide: Or( cabbage[i] == 0 , cabbage[i] == 1 )
goatSide: Or( goat[i] == 0 , goat[i] == 1 )
humanSide: Or( human[i] == 0 , human[i] == 1 )
t7: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
t3: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] + 1 )
t6: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] - 1 )
t2: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage == cabbage[i] )
t5: And( And( And( humanTravel[i] , wolf == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage == cabbage[i] )
t1: And( And( And( humanTravel[i] , wolf == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
t4: And( And( And( humanTravel[i] , wolf == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage == cabbage[i] )
safeAlone: And( goat[i+1] != wolf , goat[i+1] != cabbage )
wolfSide: Or( wolf[i] == 0 , wolf[i] == 1 )
humanTravel: human[i] != human[i+1]
side: And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] )
safe: Or( safeAlone[i] , goat[i+1] == human[i+1] )
objectTravel: Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] )
data: And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] )
ืื ืืืืื ืืื ืืขื ืืขื ืขื ืืืืกืืขืฉืืขืื ืืื ืื ืกืขืจืืึทื ืืื ืึท ืฉืจืืคื ืืืกืืขืจ ืืืืืื ื ืฆื ืืึทืฉืจืืึทืื ืื ืกืื ืกืืกืืขื ืืื ืคึผืืืืึธื.
ืืืืืืง ืืืกืืขืจ
import json
from z3 import *
s = Solver()
Steps=7
Num= Steps+1
$code$
#template, only start rest
s.add(data + start)
#template
s.add(final)
ind = 0
f = open("/var/www/html/all/bin/python/log.txt", "a")
while s.check() == sat:
ind = ind +1
print ind
m = s.model()
print m
print "traversing model..."
#for d in m.decls():
#print "%s = %s" % (d.name(), m[d])
f.write(str(m))
f.write("nn")
exit()
#s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model
print "Total solution number: "
print ind
f.close()
ืคึฟืึทืจ ืื ืืขืฆืืข ืฉืืึทื ืืื ืื ืืื ืฆืข ืงืืื, ืื ืึผืืืื ืืืึธืก ืืขื ืขื ืกืคึผืขืกืืคืืขื ืืื ืื ืึทืจืืืขืจืคืืจื ืืจืึทื ืกืึทืงืืืึธื ืึธืคึผืืืืืื ื ืืขื ืขื ืืขืืืขื ืื.
ืืขื ืืืื ืึทื Z3Prover ืืืขื ืงืืงื ืคึฟืึทืจ ืคึผืื ืงื ืึทืืึท ืกืขื ืคืื ืืืืื ืืื ืืขื ืืืึธืก ืืขืกืึธืฃ ืืึธืื ืืขืื ืฆื ืืืื ืืืืืืจืึธื ืคืื ืื ืงืึธื ืืจืึทืงื.
ืืื ืึท ืจืขืืืืืึทื, ืืืจ ืืืืืึธืืึทืืืฉ ืืึทืงืืืขื ืึท ืืึธืจ ืคืึทื ืืงืฉืึทื ืึทื ืกืื ืืึธืืขื ืคืื ืืื ืืืขืจ ืงืึธื ืืจืึทืงื.
ืืืจ ืงืขื ืขื ืืขื ืึทื ืขืก ืืื ืืืืขืจ ืขื ืืขื ืฆื ืื ืืึธืืขื ืคืื ืืืื ืคืจืืขืจืืืงื ืึทืจืืืงื, ืืืึธืก ืืื ืฆืื ืืืคืืขืฉืืขืื ืืึทื ืืืึทืื.
ืืขืขื ืืืงื ืืืกืืขืจ
import json
from z3 import *
s = Solver()
Steps=7
Num= Steps+1
human = [ Int('human_%i' % (i + 1)) for i in range(Num) ]
wolf = [ Int('wolf_%i' % (i + 1)) for i in range(Num) ]
goat = [ Int('goat_%i' % (i + 1)) for i in range(Num) ]
cabbage = [ Int('cabbage_%i' % (i + 1)) for i in range(Num) ]
nothing= [ And( human[i] == human[i+1], wolf[i] == wolf[i+1], goat[i] == goat[i+1], cabbage[i] == cabbage[i+1] ) for i in range(Num-1) ]
start= [ human[0] == 1, wolf[0] == 0, goat[0] == 1, cabbage[0] == 0 ]
safeAlone= [ And( goat[i+1] != wolf[i+1] , goat[i+1] != cabbage[i+1] ) for i in range(Num-1) ]
safe= [ Or( safeAlone[i] , goat[i+1] == human[i+1] ) for i in range(Num-1) ]
humanTravel= [ human[i] != human[i+1] for i in range(Num-1) ]
cabbageSide= [ Or( cabbage[i] == 0 , cabbage[i] == 1 ) for i in range(Num-1) ]
goatSide= [ Or( goat[i] == 0 , goat[i] == 1 ) for i in range(Num-1) ]
humanSide= [ Or( human[i] == 0 , human[i] == 1 ) for i in range(Num-1) ]
t7= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t3= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] + 1 ) for i in range(Num-1) ]
t6= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] - 1 ) for i in range(Num-1) ]
t2= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] + 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t5= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] ) , goat[i+1] == goat[i] - 1 ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t1= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] + 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
t4= [ And( And( And( humanTravel[i] , wolf[i+1] == wolf[i] - 1 ) , goat[i+1] == goat[i] ) , cabbage[i+1] == cabbage[i] ) for i in range(Num-1) ]
wolfSide= [ Or( wolf[i] == 0 , wolf[i] == 1 ) for i in range(Num-1) ]
side= [ And( And( And( humanSide[i] , wolfSide[i] ) , goatSide[i] ) , cabbageSide[i] ) for i in range(Num-1) ]
objectTravel= [ Or( Or( Or( Or( Or( Or( t1[i] , t2[i] ) , t3[i] ) , t4[i] ) , t5[i] ) , t6[i] ) , t7[i] ) for i in range(Num-1) ]
data= [ Or( And( And( And( side[i] , safe[i] ) , humanTravel[i] ) , objectTravel[i] ) , nothing[i]) for i in range(Num-1) ]
fState= And( And( And( human[Steps] == 1 , wolf[Steps] == 1 ) , goat[Steps] == 1 ) , cabbage[Steps] == 1 )
final= fState
#template, only start rest
s.add(data + start)
#template
s.add(final)
ind = 0
f = open("/var/www/html/all/bin/python/log.txt", "a")
while s.check() == sat:
ind = ind +1
print ind
m = s.model()
print m
print "traversing model..."
#for d in m.decls():
#print "%s = %s" % (d.name(), m[d])
f.write(str(m))
f.write("nn")
exit()
#s.add(Or(goat[0] != s.model()[data[0]] )) # prevent next model from using the same assignment as a previous model
print "Total solution number: "
print ind
f.close()
ื ืึธื ืงืึทืืขืจ, Z3Prover ืกืึทืืืื ืื ืงืืื ืงืึธื ืืจืึทืงื ืืื ืืื ืืื ืื ืึท ืงืืื ืคืื ืืจืึทื ืืึทืงืฉืึทื ื ืืืึธืก ืืึธืื ืืื ืื ืฆืืจืืงืฆืืขื ืืขืื:
Winning transaction chain found:
Data transaction: human= 0, wolf= 0, goat= 1, cabbage= 0
Data transaction: human= 1, wolf= 0, goat= 1, cabbage= 1
Data transaction: human= 0, wolf= 0, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 0, wolf= 1, goat= 0, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Data transaction: human= 1, wolf= 1, goat= 1, cabbage= 1
Transfer transaction
ืืื ืึทืืืฉืึทื ืฆื ืื ืคึผืจืึธื ืงืึธื ืืจืึทืงื, ืืืจ ืงืขื ืขื ืขืงืกืคึผืขืจืืืขื ื ืืื ืืืื ืืืืืขื ืข ืงืึทื ืืจืึทืงืฅ ืึธืืขืจ ืคึผืจืืืืจื ืืขื ืคึผืฉืื ืืืึทืฉืคึผืื, ืืืึธืก ืืื ืกืึทืืืื ืืื 2 ืืจืึทื ืืึทืงืฉืึทื ื.
let contract = tx.sender
let a= extract(getInteger(contract,"a"))
let b= extract(getInteger(contract,"b"))
let c= extract(getInteger(contract,"c"))
let d= extract(getInteger(contract,"d"))
match tx {
case t:DataTransaction =>
let na= extract(getInteger(t.data,"a"))
let nb= extract(getInteger(t.data,"b"))
let nc= extract(getInteger(t.data,"c"))
let nd= extract(getInteger(t.data,"d"))
nd == 0 || a == 100 - 5
case s:TransferTransaction =>
( a + b - c ) * d == 12
case _ => true
}
ืืื ื ืืึธืก ืืื ืืขืจ ืขืจืฉืืขืจ ืืืขืจืกืืข, ืื ืกืื ืืึทืงืก ืืื ืืืืขืจ ืืืืืืขื ืืื ืขืก ืงืขื ืืืื ืืึทืื.
ืืื ืื ืคืืืืขื ืืข ืึทืจืืืงืืขื, ืืื ืคึผืืึทื ืฆื ืืขืงื ืื ืืืืึทืืขืจ ืึทื ืืืืืงืืื ื ืคืื ืื VM, ืืื ืืืืึทืื ืืื ืืืจ ืงืขื ืขื ืืึทืื ืคืึธืจืืึทืื ืืืขืจืึทืคืืื ืงืืื ืงืึทื ืืจืึทืงืฅ ืืื ืืืื ืืืืฃ, ืืื ื ืื ื ืึธืจ ืกืึธืืืืข ืืื.
ืืขืจ ืืึทืจืึทืงืืขืจ ืืืืจืืืึทื ืืึทืฉืื ืืื ืื ืืืฆื ืืื
ื ืึธื ืฉืืขืื ืื ืืงืืจ ืงืึธื ืคืื ืื ืกืืืืึธืืืฉ VM ืืื ืกืืจ ืืื ืึทืืื ื ืืึทืืขืจืงืื ืืขื ืืึธืจื, ืืื ืคึผืืึทื ืฆื ืฉืืขืื ืขืก ืืืืฃ GitHub ืคึฟืึทืจ ืคืจืื ืึทืงืกืขืก.
ืืงืืจ: www.habr.com