ນີ້ແມ່ນຕົວກວດສອບຄໍາສັ່ງທີ່ສາມາດດໍາເນີນການໄດ້ໃນ OnWorks ຜູ້ໃຫ້ບໍລິການໂຮດຕິ້ງຟຣີໂດຍໃຊ້ຫນຶ່ງໃນຫຼາຍສະຖານີເຮັດວຽກອອນໄລນ໌ຂອງພວກເຮົາເຊັ່ນ Ubuntu Online, Fedora Online, Windows online emulator ຫຼື MAC OS online emulator
ໂຄງການ:
NAME
checker - SPARK Proof Checker
ສະຫຼຸບສັງລວມ
checker [ຕົວເລືອກ] [ເອກະສານ]
ລາຍລະອຽດ
ເຄື່ອງກວດພິສູດຫຼັກຖານ SPARK ສາມາດຖືກນໍາໃຊ້ເພື່ອປົດປ່ອຍເງື່ອນໄຂການກວດສອບທີ່ຜະລິດໂດຍ
Examiner (*.vcg), ອາດຈະເຮັດໃຫ້ງ່າຍດາຍໂດຍ Simplifier (*.siv). ຄໍາສັ່ງນີ້ແມ່ນປົກກະຕິແລ້ວ
ໃຊ້ໃນເວລາທີ່ເງື່ອນໄຂການຢັ້ງຢືນບໍ່ສາມາດຖືກປ່ອຍອັດຕະໂນມັດໂດຍ Simplifier.
ໂດຍຄ່າເລີ່ມຕົ້ນ checker ແລ່ນຢູ່ໃນໂໝດໂຕ້ຕອບ. ມັນຍອມຮັບຄໍາສັ່ງຈາກຜູ້ໃຊ້ແລະຂຽນ
ໃຫ້ເຂົາເຈົ້າເຂົ້າໄປໃນໄຟລ໌ cmd (ຫຼືໄຟລ໌ອື່ນໆທີ່ລະບຸໄວ້ໂດຍ -command_log ທາງເລືອກ). ໄຟລ໌ນີ້ສາມາດເປັນ
ໃຊ້ຕໍ່ມາເພື່ອແລ່ນ checker ໃນຮູບແບບ batch (ການນໍາໃຊ້ທາງເລືອກ - ປະຕິບັດ). ນອກຈາກນັ້ນ, ບັນທຶກຫຼັກຖານ
ຖືກຂຽນໄວ້ໃນໄຟລ໌ plg.
OPTIONS
ສະຫຼຸບຂອງທາງເລືອກແມ່ນລວມຢູ່ຂ້າງລຸ່ມນີ້. ຕົວເລືອກທັງໝົດອາດຈະຖືກຫຍໍ້ໃຫ້ສັ້ນທີ່ສຸດ
ຄໍານໍາຫນ້າເປັນເອກະລັກ.
-ຊ່ວຍ ສະແດງສະຫຼຸບຂອງທາງເລືອກ.
-ການປ່ຽນແປງ
ສະແດງຂໍ້ມູນສະບັບ.
- ທຳ ມະດາ ນຳໃຊ້ຮູບແບບຜົນຜະລິດແບບທຳມະດາ (ເຊັ່ນ: ບໍ່ມີວັນທີ ຫຼືຕົວເລກເວີຊັນ).
-overwrite_warning
ການຢືນຢັນທີ່ຈໍາເປັນເພື່ອຂຽນທັບຄໍາສັ່ງຫຼືໄຟລ໌ບັນທຶກຫຼັກຖານ.
-command_log=LOG_FILE
ລະບຸຊື່ໄຟລ໌ສໍາລັບໄຟລ໌ບັນທຶກຄໍາສັ່ງ.
-proof_log=PLG_FILE
ລະບຸຊື່ໄຟລ໌ສໍາລັບໄຟລ໌ບັນທຶກຫຼັກຖານ.
-execute=LOG_FILE
ປະຕິບັດໄຟລ໌ບັນທຶກຄໍາສັ່ງທີ່ສ້າງຂຶ້ນກ່ອນຫນ້ານີ້.
ບັນຊີ
ສືບຕໍ່ເຊດຊັນທີ່ບັນທຶກໄວ້ໃນເມື່ອກ່ອນ.
ໃຊ້ຕົວກວດສອບອອນໄລນ໌ໂດຍໃຊ້ບໍລິການ onworks.net
