ការបង្កើតប្រព័ន្ធផ្ទៀងផ្ទាត់ជាផ្លូវការពីដំបូង។ ផ្នែកទី 1: ម៉ាស៊ីននិម្មិតតួអក្សរនៅក្នុង PHP និង Python

ការផ្ទៀងផ្ទាត់ជាផ្លូវការគឺជាការផ្ទៀងផ្ទាត់កម្មវិធីមួយ ឬក្បួនដោះស្រាយដោយប្រើកម្មវិធីផ្សេងទៀត។

នេះគឺជាវិធីសាស្រ្តដ៏មានឥទ្ធិពលបំផុតមួយ ដែលអនុញ្ញាតឱ្យអ្នកស្វែងរកភាពងាយរងគ្រោះទាំងអស់នៅក្នុងកម្មវិធី ឬបង្ហាញថាវាមិនមាន។

ការពិពណ៌នាលម្អិតបន្ថែមទៀតនៃការផ្ទៀងផ្ទាត់ជាផ្លូវការអាចមើលឃើញនៅក្នុងឧទាហរណ៍នៃការដោះស្រាយបញ្ហានៃ ចចក ពពែ និងស្ពៃក្តោប នៅក្នុងអត្ថបទមុនរបស់ខ្ញុំ។

នៅក្នុងអត្ថបទនេះខ្ញុំផ្លាស់ប្តូរពីការផ្ទៀងផ្ទាត់ជាផ្លូវការនៃបញ្ហាទៅជាកម្មវិធី ហើយពិពណ៌នាអំពីរបៀប
តើពួកគេអាចបំប្លែងទៅជាប្រព័ន្ធច្បាប់ផ្លូវការដោយស្វ័យប្រវត្តបានដោយរបៀបណា។

ដើម្បីធ្វើដូចនេះខ្ញុំបានសរសេរ analogue ផ្ទាល់ខ្លួនរបស់ខ្ញុំនៃម៉ាស៊ីននិម្មិតដោយប្រើគោលការណ៍និមិត្តសញ្ញា។

វាញែកកូដកម្មវិធី ហើយបកប្រែវាទៅជាប្រព័ន្ធសមីការ (SMT) ដែលអាចត្រូវបានដោះស្រាយតាមកម្មវិធីរួចហើយ។

ដោយសារព័ត៌មានអំពីការគណនានិមិត្តសញ្ញាត្រូវបានបង្ហាញនៅលើអ៊ីនធឺណិតជាផ្នែកៗ។
ខ្ញុំនឹងរៀបរាប់ដោយសង្ខេបថាវាជាអ្វី។

ការគណនានិមិត្តសញ្ញាគឺជាវិធីមួយដើម្បីដំណើរការកម្មវិធីក្នុងពេលដំណាលគ្នានៅលើជួរទិន្នន័យដ៏ធំទូលាយ និងជាឧបករណ៍ចម្បងសម្រាប់ការផ្ទៀងផ្ទាត់កម្មវិធីផ្លូវការ។

ឧទាហរណ៍ យើងអាចកំណត់លក្ខខណ្ឌបញ្ចូល ដែលអាគុយម៉ង់ទីមួយអាចយកតម្លៃវិជ្ជមានណាមួយ អវិជ្ជមានទីពីរ សូន្យទីបី និងអាគុយម៉ង់លទ្ធផល ឧទាហរណ៍ 42។

ការគណនានិមិត្តសញ្ញានៅក្នុងការរត់មួយនឹងផ្តល់ឱ្យយើងនូវចម្លើយថាតើវាអាចទៅរួចសម្រាប់យើងដើម្បីទទួលបានលទ្ធផលដែលចង់បាននិងឧទាហរណ៍នៃសំណុំនៃប៉ារ៉ាម៉ែត្របញ្ចូលបែបនេះ។ ឬភស្តុតាងថាមិនមានប៉ារ៉ាម៉ែត្របែបនេះទេ។

លើស​ពី​នេះ​ទៅ​ទៀត យើង​អាច​កំណត់​អាគុយម៉ង់​បញ្ចូល​ទៅ​គ្រប់​អ្វី​ដែល​អាច​ធ្វើ​បាន ហើយ​ជ្រើស​យក​តែ​ធាតុ​លទ្ធផល​ប៉ុណ្ណោះ ឧទាហរណ៍ ពាក្យ​សម្ងាត់​អ្នក​គ្រប់គ្រង។

ក្នុងករណីនេះ យើងនឹងរកឃើញភាពងាយរងគ្រោះរបស់កម្មវិធីទាំងអស់ ឬទទួលបានភស្តុតាងថាពាក្យសម្ងាត់របស់អ្នកគ្រប់គ្រងមានសុវត្ថិភាព។

វាអាចត្រូវបានកត់សម្គាល់ថាការប្រតិបត្តិបុរាណនៃកម្មវិធីដែលមានទិន្នន័យបញ្ចូលជាក់លាក់គឺជាករណីពិសេសនៃការប្រតិបត្តិនិមិត្តសញ្ញា។

ដូច្នេះ VM តួអក្សររបស់ខ្ញុំក៏អាចដំណើរការក្នុងរបៀបត្រាប់តាមម៉ាស៊ីននិម្មិតស្តង់ដារផងដែរ។

នៅក្នុងមតិយោបល់ទៅអត្ថបទមុន គេអាចរកឃើញការរិះគន់ដោយយុត្តិធម៌នៃការផ្ទៀងផ្ទាត់ជាផ្លូវការជាមួយនឹងការពិភាក្សាអំពីភាពទន់ខ្សោយរបស់វា។

បញ្ហាចម្បងគឺ៖

1. ការផ្ទុះរួមគ្នាចាប់តាំងពីការផ្ទៀងផ្ទាត់ជាផ្លូវការនៅទីបំផុតបានធ្លាក់ចុះដល់ P=NP
2. ការដំណើរការការហៅទៅកាន់ប្រព័ន្ធឯកសារ បណ្តាញ និងកន្លែងផ្ទុកខាងក្រៅផ្សេងទៀតគឺពិបាកក្នុងការផ្ទៀងផ្ទាត់
3. កំហុសនៅក្នុងការបញ្ជាក់ នៅពេលដែលអតិថិជន ឬអ្នកសរសេរកម្មវិធីមានបំណងអ្វីមួយ ប៉ុន្តែមិនបានពិពណ៌នាវាឱ្យត្រឹមត្រូវគ្រប់គ្រាន់នៅក្នុងលក្ខណៈបច្ចេកទេសនោះទេ។

ជាលទ្ធផល កម្មវិធីនឹងត្រូវបានផ្ទៀងផ្ទាត់ និងអនុលោមតាមការបញ្ជាក់ ប៉ុន្តែនឹងធ្វើអ្វីមួយខុសពីអ្វីដែលអ្នកបង្កើតរំពឹងទុកពីវា។

ដោយសារនៅក្នុងអត្ថបទនេះខ្ញុំកំពុងពិចារណាជាចម្បងលើការប្រើប្រាស់ការផ្ទៀងផ្ទាត់ជាផ្លូវការក្នុងការអនុវត្ត ខ្ញុំនឹងមិនវាយក្បាលខ្ញុំទល់នឹងជញ្ជាំងសម្រាប់ពេលនេះទេ ហើយនឹងជ្រើសរើសប្រព័ន្ធដែលភាពស្មុគស្មាញនៃក្បួនដោះស្រាយ និងចំនួននៃការហៅខាងក្រៅមានតិចតួចបំផុត។

ដោយសារកិច្ចសន្យាឆ្លាតវៃស័ក្តិសមបំផុតនឹងតម្រូវការទាំងនេះ ជម្រើសបានធ្លាក់លើកិច្ចសន្យា RIDE ពីវេទិកា Waves៖ ពួកគេមិនបានបញ្ចប់ Turing ហើយភាពស្មុគស្មាញអតិបរមារបស់ពួកគេត្រូវបានកំណត់ដោយសិប្បនិម្មិត។

ប៉ុន្តែយើងនឹងពិចារណាពួកវាទាំងស្រុងពីផ្នែកបច្ចេកទេស។

បន្ថែមពីលើអ្វីៗទាំងអស់ ការផ្ទៀងផ្ទាត់ជាផ្លូវការនឹងមានតម្រូវការជាពិសេសសម្រាប់កិច្ចសន្យាណាមួយ៖ ជាធម្មតាវាមិនអាចទៅរួចទេក្នុងការកែកំហុសកិច្ចសន្យាបន្ទាប់ពីវាត្រូវបានដាក់ឱ្យដំណើរការ។
ហើយតម្លៃនៃកំហុសបែបនេះអាចខ្ពស់ណាស់ ព្រោះថាចំនួនទឹកប្រាក់ដ៏ច្រើនត្រូវបានរក្សាទុកនៅលើកិច្ចសន្យាឆ្លាតវៃ។

ម៉ាស៊ីននិម្មិតនិម្មិតរបស់ខ្ញុំត្រូវបានសរសេរជា PHP និង Python ហើយប្រើ Z3Prover ពី Microsoft Research ដើម្បីដោះស្រាយរូបមន្ត SMT លទ្ធផល។

នៅស្នូលរបស់វាគឺការស្វែងរកពហុប្រតិបត្តិការដ៏មានឥទ្ធិពល, ដែល
អនុញ្ញាតឱ្យអ្នកស្វែងរកដំណោះស្រាយ ឬភាពងាយរងគ្រោះ ទោះបីជាវាត្រូវការប្រតិបត្តិការជាច្រើនក៏ដោយ។
សូម្បីតែ Mythrilដែលជាក្របខ័ណ្ឌនិមិត្តសញ្ញាដ៏មានឥទ្ធិពលបំផុតមួយសម្រាប់ការស្វែងរកភាពងាយរងគ្រោះ Ethereum ទើបតែបានបន្ថែមសមត្ថភាពនេះកាលពីប៉ុន្មានខែមុនប៉ុណ្ណោះ។

ប៉ុន្តែវាគួរឱ្យកត់សម្គាល់ថាកិច្ចសន្យាអេធើរគឺស្មុគស្មាញជាងហើយ Turing បានបញ្ចប់។

PHP បកប្រែកូដប្រភពនៃកិច្ចសន្យាឆ្លាតវៃ RIDE ទៅជាស្គ្រីប python ដែលក្នុងនោះកម្មវិធីត្រូវបានបង្ហាញជាប្រព័ន្ធ Z3 SMT-compatible នៃកិច្ចសន្យា និងលក្ខខណ្ឌសម្រាប់ការផ្លាស់ប្តូររបស់ពួកគេ៖

ឥឡូវនេះខ្ញុំនឹងរៀបរាប់អំពីអ្វីដែលកំពុងកើតឡើងនៅខាងក្នុងយ៉ាងលម្អិតបន្ថែមទៀត។

ប៉ុន្តែជាដំបូង ពាក្យពីរបីអំពីភាសាកិច្ចសន្យាឆ្លាតវៃ RIDE ។

វាជាភាសាសរសេរកម្មវិធីដែលមានមុខងារ និងការបញ្ចេញមតិ ដែលខ្ជិលតាមការរចនា។
RIDE ដំណើរការក្នុងភាពឯកោនៅក្នុង blockchain ហើយអាចទាញយក និងសរសេរព័ត៌មានពីការផ្ទុកដែលភ្ជាប់ទៅនឹងកាបូបរបស់អ្នកប្រើ។

អ្នកអាចភ្ជាប់កិច្ចសន្យា 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-compatible system description នៅក្នុង Python។
ទិន្នន័យត្រូវបានរុំនៅក្នុងរង្វិលជុំដែលអថេរផ្ទុកទទួលបានសន្ទស្សន៍ i សន្ទស្សន៍ប្រតិបត្តិការអថេរ 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] )  

លក្ខខណ្ឌត្រូវបានតម្រៀប និងបញ្ចូលទៅក្នុងគំរូស្គ្រីបដែលត្រូវបានរចនាឡើងដើម្បីពិពណ៌នាអំពីប្រព័ន្ធ SMT នៅក្នុង Python ។

គំរូទទេ

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 នឹងស្វែងរកយ៉ាងជាក់លាក់នូវលក្ខខណ្ឌបែបនេះដែលនឹងអនុញ្ញាតឱ្យដកប្រាក់ចេញពីកិច្ចសន្យា។

ជាលទ្ធផល យើងទទួលបានគំរូ SMT ដែលមានមុខងារពេញលេញនៃកិច្ចសន្យារបស់យើងដោយស្វ័យប្រវត្តិ។
អ្នកអាចមើលឃើញថាវាស្រដៀងទៅនឹងគំរូពីអត្ថបទមុនរបស់ខ្ញុំ ដែលខ្ញុំបានចងក្រងដោយដៃ។

គំរូដែលបានបញ្ចប់

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 និងបង្ហាញពីរបៀបដែលអ្នកអាចបង្កើតកិច្ចសន្យាឆ្លាតវៃដែលត្រូវបានផ្ទៀងផ្ទាត់ជាផ្លូវការជាមួយនឹងជំនួយរបស់វា ហើយមិនត្រឹមតែដោះស្រាយវាប៉ុណ្ណោះទេ។

ម៉ាស៊ីននិម្មិតតួអក្សរមាននៅ http://2.59.42.98/hyperbox/
បន្ទាប់ពីដាក់កូដប្រភពនៃនិមិត្តសញ្ញា VM តាមលំដាប់លំដោយ និងបន្ថែមមតិយោបល់នៅទីនោះ ខ្ញុំមានគម្រោងដាក់វានៅលើ GitHub ដោយឥតគិតថ្លៃ។

ប្រភព: www.habr.com