Multithreading in SPIN model checker -

-

how parametrize spin model number of threads? using standard spin model checker. have options set number of parallel threads? checked reference didn't find useful

you can dynamically spawn promela process using run operator. can iterate as:

#define try_count 5 byte index = 0; :: index == try_count -> break :: else -> index++; run theprocess() od

you can define file like:

active [try_count] proctype foo () {   printf ("pid: %d\n", _pid);   assert (true) }  init {   assert (true) }

and run spin simulation:

$ spin -dtry_count=4 bar.pml               pid: 2       pid: 0           pid: 1                   pid: 3 5 processes created

or verification

$ spin -dtry_count=4 -a bar.pml $ gcc -o bar pan.c $ ./bar hint: search more efficient if pan.c compiled -dsafety  (spin version 6.3.2 -- 17 may 2014)     + partial order reduction ...

Comments

Post a Comment

Popular posts from this blog

javascript - How to synchronize the Three.js and HTML/SVG coordinate systems (especially w.r.t. the y-axis)? -

-
i'm combining 3d content three.js html , svg content. three.js cssloader pretty job synchronizing placement of html , svg content in 3d world. but svg/html coordinate systems 'left-handed', whereas three.js coordinate system 'right-handed'. means y-axes reversed. in svg/html, y / top goes go down screen, , three.js uses more standard mathematical convention of y going down go down screen. i have continually convert 1 other, pretty error prone. know not first run (for example, look here ). has come general solution? here's tried: do in object3d .scale.y = -1 . may suspect, turns out disaster. turns inside-out, , don't try put camera in there. do in object3d .rotate.x = math.pi . more promising, z axis no longer consistent html concept of z-index. still, i'm using now. in html, don't use top , use bottom . in svg , inside <g transform="scale(1, -1)"> inside <g transform="translate(0, imageheight)"> . h...
Read more

javascript - How do I find how many occurences are there of a highlighted string, and which occurence is it? -

-
as title says, have website text inside div, there way highlight part of , know occurence is? if text has 4 occurences of word "something", , highlight 3rd, how information using javascript/jquery? http://jsfiddle.net/g09g35xa/6/ here's method seems work. highlight string want , when click button alert index of highlighted word in div. markup: <div id="thediv"> <p>the quick brown quick fox jumps on lazy dog</p> </div> <br /> <input id="findindex" type="button" value="find index of highlighted string" /> and js: function getselectedhtml() { try { if (window.activexobject) { var c = document.selection.createrange(); return c.htmltext; } return getselection().getrangeat(0).tostring(); } catch (e) { if (window.activexobject) { return document.selection.createrange(); } else { return ...
Read more

java - Reading data from multiple zip files and combining them to one -

-
i want read data lets 4 zip files called zip1, zip2, zip3, zip4. of these zip files split 1 big zip file called "bigzip". want combine zip files 1 , compare bytes if 1 bigzip file matches size of bytes combined zip file of (zip1+zip2+zip3+zip4). getting small file size when combine size of 4 zip files. doing wrong? here code same: targetfilepath1, targetfilepath2, targetfilepath3, targetfilepath4 belongs path of 4 zip files. sourcefilepath path bigzip file class test { public static void main(string args[]) { zipoutputstream outstream = new zipoutputstream(new fileoutputstream(sourcebigzip)); readzip(sourcefilepath, targetfilepath1); readzip(sourcefilepath, targetfilepath2); readzip(sourcefilepath, targetfilepath3); readzip(sourcefilepath, targetfilepath4); outstream.close(); } static void readzip(string sourcebigzip, string targetfile) throws exception { zipinputstream instream = new zipinputstream(new file...
Read more