[[start|{{:home.png?16}}]][[start| Main]]
[[release|{{:tool.png?16}}]][[release| Tool ]]
[[contact|{{:letter.png?16}}]][[contact| Contact ]]

=====How to use the tool=====
After downloading the .zip file, first please refer to this page to build ePMC:[[https://github.com/ISCAS-PMC/ePMC/wiki/Documentations|wiki:ePMC]].

To perform dpCTL model checking, please set the following options:

<code>
--property-solver propositional-explicit,operator-explicit,pctl-explicit-next,dpctl-explicit-knowledge,dpctl-explicit-until
--prism-flatten false
--model-input-type mas
--property-input-type dpctl
--smtlib-command-line z3 -smt2 {0} 
--smtlib-version v25
--constraintsolver-solver smt-lib 
--model-input-files /path/to/your-model
--property-input-files /path/to/your-property
</code>

In order to use our tool, a model file and a property file is request, following the standards of PRISM format([[http://www.prismmodelchecker.org/manual/ThePRISMLanguage|ThePRISMLanguage]]). To specify the differentially private properties, a new operator  $D\{\epsilon,\delta\}[Pathformula]$ is introduced,
and it will tell the model checker to check that for any initial states $s_1$ and $s_2$(assumed in neighborhood relations), whether 

$Pr(s_1\models Pathformula) \le e^{\epsilon} Pr(s_2\models Pathformula) + \delta $

holds. If there's a violation of the formula, differential privacy is not achieved and a counterexample of  $s_1$ and $s_2$, along with the probabilities will be given. Otherwise, the model checker returns an answer "yes". Examples of formulae are shown below:


==D {3, 0} [F (1 < s & s <= 2) ]== 

==D {1, 0} [X ((d = -1) & (t = -1) )]==

=====Simple case study=====

Below are the model file(MDP) and property file of a survey mechanism with high/low accuracy.

<code java>
mdp

module M1

	// local state
	s : [0..3] ;

	[a] s=0 -> 0.75 : (s'=2) + 0.25 : (s'=3);
	[b] s=0 -> 0.8 : (s'=2) + 0.2 : (s'=3);
	[a] s=1 -> 0.25 : (s'=2) + 0.75 : (s'=3);
	[b] s=0 -> 0.2 : (s'=2) + 0.8 : (s'=3);
endmodule

init s = 0  | s = 1 endinit
</code>

The model is like this in the original paper[3]:

{{:1605697988.png?400|}}

And the property file:

<code java>
e = 2.71828183
D{log(3,e),0} [F (s=2 | s=3)]
D{log(4,e),0} [F (s=2 | s=3)]
</code>

The second property with $\epsilon = \ln 4$ is the only one to be satisfied.