Simplified form of the RANSAC algorithm

Introduction

This is the RoboChart model corresponding to the simplified form of the RANSAN algorithm in Chapter 8 of the RoboSoft paper: “RoboStar Technology: Modelling Uncertainty in RoboChart using Probability” by Jim Woodcock et al. Authors intend to use Hehner’s probabilistic predicative programming to prove this simplified form.

We use this model and its probabilistic verification using PRISM to reassure the proof is correct.

A brief description of the simplified form

Let D be a dataset and contains N data points. In order to fit a model, we need at least 2 data points. For a valid model, these data points contain at least two inliers (d=2). We also estimate the probability of one data point in D is an outlier in the model with the current parameters as q.

This model aims to determine how many iterations are needed, on average, to find the first sample without outliers for this dataset.

The paper has proved, on average, it needs 1.7 iterations for N=6 and q=1/3.

V1

Model (download)

We consider N is 6 and q is 1/3, defined as the constants in the model.

We use a uniform selection algorithm twice to randomly choose two indices from the data set as modelled in the state machine simpRansacSTM. It declares a variable i of type nat to denote the output index of the algorithm. Another two variables index0 and index1 are just the chosen indices. A value -1 indicates the index has not been chosen.

The uniform selection algorithm is implemented by a probabilistic junction between ChooseIndex and UpdateChosenIndex. The table below shows how the algorithm works and the resulted distribution.

Steps	i	p_{Repeat} [R]	p_{UpdateChosenIndex} [U]	Accumulation
1	0	5/6 [R]	1/6 [U]	1/6 [U]
2	1	4/5 [R]	1/5 [U]	5/6*1/5 = 1/6 [RU]
3	2	3/4 [R]	1/4 [U]	5/6*4/5*1/4 = 1/6 [RRU]
4	3	2/3 [R]	1/3 [U]	5/6*4/5*3/4*1/3 = 1/6 [RRRU]
5	4	1/2 [R]	1/2 [U]	5/6*4/5*3/4*2/3*1/2 = 1/6 [RRRRU]
6	5	0 [R]	1/1 [U]	5/6*4/5*3/4*2/3*1/2*1 = 1/6 [RRRRRU]

As you can see, we get a uniform distribution on i: [(0, 1/6), (1, 1/6), (2, 1/6), (3, 1/6), (4, 1/6), (5, 1/6)].

Using this algorithm with a binary choice operator P, we can implement a uniform distribution for any number of N.

Analysis

Generated PRISM model (download)

Used configuration file.

Assertions

The assertion file (download) that is used for verification is shown below.

Reports

The verification results are displayed in the report below.

---

Assertion: P_deadlock_free

Assertion	States	Transitions	Time	Result
P_deadlock_free	591	686	0.002 seconds	true

Assertion: P_nr_of_tries

Assertion	States	Transitions	Time	Result
P_nr_of_tries	591	686	0.039 seconds	1.6998580815632656

Assertion: P_nr_of_choices

Assertion	States	Transitions	Time	Result
P_nr_of_choices	591	686	0.027 seconds	2.6998493976687925

---

The result of P_nr_of_choose gives us the average number of occurrences of the choose event: 2.6998.

The result of P_nr_of_tries gives us the average number of entries to the badFit state: 1.6998, which is consistent with the result 1.7 by theorem proving.

V2

Model (download)

In this version, we use an operation ChooseUniform to implement the uniform selection algorithm.

Then in the state machine, this operation is called twice to select indices for index0 and index1.

Analysis

Generated PRISM model (download)

Used configuration file.

Assertions

The assertion file (download) that is used for verification is shown below.

Reports

The verification results are displayed in the report below.

---

Assertion: P_deadlock_free

Assertion	states:	transitions:	result:	checkTime:
P_deadlock_free	3615	4070	true	0.003 seconds

Assertion: P_nr_of_tries

Assertion	states:	transitions:	result:	checkTime:
P_nr_of_tries	3615	4070	1.6998561958204306	0.117 seconds

Assertion: P_nr_of_choices

Assertion	states:	transitions:	result:	checkTime:
P_nr_of_choices	3615	4070	2.6998527952527036	0.115 seconds

Assertion: P_goodfit

Assertion	states:	transitions:	result:	checkTime:
P_goodfit	3615	4070	1.0	0.043 seconds

---

The results of P_nr_of_choose and P_nr_of_tries of V2 are consistent with those of V1.

Conclusion

This example shows the probabilistic analysis of a RoboChart model by modeling checking can be used in a complementary way to theorem proving.

In the future, we will bring the proving capability into RoboTool, and so we can use both model checking and theorem proving for analysis together.