Python script

A developer configures T-Check using an extended version of TOSSIM's configuration mechanism, via a Python script.

Users can refer to TOSSIM link to learn how to write the python script for TOSSIM. In addition to APIs currently provided by TOSSIM, T-Check extends the following APIs.

• initMoteNum(int moteNum, int propertyNum) : tells T-Check how many motes and sets of property will be involved in T-Check initially, this function should always be called in the first place;
• setLossAndBiasingAndTossim(int loss_mode, int bias_mode, int tossim_mode) : sets loss mode, biasing mode and TOSSIM-supporting mode for T-Check.
• loss mode, which controls the packet loss, has four options:
  • No-loss: 0, the whole network does not lose any packet;
  • Loss_random: 1, the packet loss occurs randomly;
  • Loss_noise: 2, the packet loss is leaded via TOSSIM's noise model;
  • Loss_probability: 3, the packet loss is guided according to probability specified by users, and those probability is set via three set functions described below.
• biasing mode, which guides the event choosing, has two options:
  • Flattening: 0, all events among all motes should be chosen equally;
  • Biasing: 1, The communication events in a node are treated with higher probability than other events.
• TOSSIM-supporting mode has two options:
  • No-TOSSIM-support: 0;
  • TOSSIM-support: 1.
• SetDeltaDebugging(int deltaDebugging) : sets whether to shorten the error trace.
• No-debugging: 0;
• Debugging: 1;
• mcMoteDeath(int mote, int step) : mote death.
• First argument denotes mote number;
• Second argument represents the step where death occurs.
• mcMoteRevival(int mote, int step) : mote revial, often used with mcMoteDeath.
• First argument denotes mote number;
• Second argument represents the step where revival occurs.
• mcMoteReboot(int mote, int step) : mote reboot.
• First argument denotes mote number;
• Second argument represents the step where reboot occurs.
• setSendProb(double prob) : sets the packet transimission success ratio.
• setReceiveProb(double prob) : sets the packet reception success ratio.
• setAckProb(double prob) : sets the packet acknowledgement success ratio.
• startModelChecking(char* MODE, int MC_BOUND, int RW_BOUND) : sets arguments for combination of DFS and random walk.
• MODE determines what kinds of DFS will be used, classic DFS or POR-based DFS, "DFS" symbol activates classic DFS, while "DFSPOR" starts POR-based DFS;
• MC_BOUND denotes the DFS bound;
• RW_BOUND represents the bound of random walk following DFS phase, there is no random walk if this parameter is set as 0;
• startRandomWalk(int RW_BOUND, int ROUNDS) : sets arguments for pure random walk, which means there is no model checking.
• RW_BOUND denotes the random walk bound;
• ROUNDS represents the number of rounds random walk will run;

Users can refer to the example python program test.py for MultihopOscilloscope