Commit 8ccea880 authored by Ballarini Paolo's avatar Ballarini Paolo
Browse files

Upload New File

parent 57b04836
{
"cells": [
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"from numpy import *"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
"## MBMBMB...BM with two-state machines, generates description for prism\n",
"# input:\n",
"# f: vector of failure prob. for machines\n",
"# r: vector of repair prob. for machines\n",
"# b: vector of capacity buffer for buffers\n",
"# mi: initial state of machines (optional)\n",
"# bi: initial state of buffers (optional)\n",
"# prism: generate prism or not (optional)\n",
"# fn: filename for prism file (optional)\n",
"# sym: if true probs are written symbolic, otherwise numerical value\n",
"def two_state_to_prism(f,r,b,minit,binit,fn,sym):\n",
" NM=len(f)\n",
" prismfile = open(fn+\".prism\", 'w')\n",
" prismfile.write('dtmc\\n\\n')\n",
"\n",
" for i in range(NM):\n",
" prismfile.write('const double p%d=%.12e;\\n' % (i+1,f[i]))\n",
" for i in range(NM):\n",
" prismfile.write('const double r%d=%.12e;\\n' % (i+1,r[i]))\n",
" for i in range(NM-1):\n",
" prismfile.write('const int n%d=%d;\\n' % (i+1,b[i]))\n",
" for i in range(NM):\n",
" prismfile.write('const int m%dinit=%d;\\n' % (i+1,minit[i]))\n",
" for i in range(NM-1):\n",
" prismfile.write('const int b%dinit=%d;\\n' % (i+1,binit[i]))\n",
"\n",
" prismfile.write('\\nmodule ProductionLine\\n')\n",
" for i in range(NM):\n",
" prismfile.write(\"m%d: [0..1] init m%dinit;\\n\" % (i+1,i+1))\n",
" for i in range(NM-1):\n",
" prismfile.write(\"b%d: [0..n%d] init b%dinit;\\n\" % (i+1,i+1,i+1))\n",
" prismfile.write('\\n')\n",
" \n",
" everysitu=[]\n",
" for i in range(NM):\n",
" everysitu.append([0,1])\n",
" for i in range(NM-1):\n",
" everysitu.append([0,1,2]) ## 0: empty, 1: neither empty nor full, 2: full \n",
" #print(everysitu)\n",
" t=tuple([len(everysitu[i]) for i in range(2*NM-1)])\n",
" for ind in ndindex(t):\n",
" actsitu=[everysitu[i][ind[i]] for i in range(2*NM-1)]\n",
" #print(actsitu)\n",
"\n",
" prismfile.write(' [] ')\n",
" for i in range(NM):\n",
" prismfile.write('(m%d=%d)&' % (i+1,actsitu[i]))\n",
" for i in range(NM-1):\n",
" if actsitu[i+NM] == 0:\n",
" prismfile.write('(b%d=0)' % (i+1))\n",
" if actsitu[i+NM] == 1:\n",
" prismfile.write('(0<b%d)&(b%d<n%d)' % (i+1,i+1,i+1))\n",
" if actsitu[i+NM] == 2:\n",
" prismfile.write('(b%d=n%d)' % (i+1,i+1))\n",
" if i<NM-2:\n",
" prismfile.write('&')\n",
" else:\n",
" prismfile.write(' ->')\n",
" \n",
" fm=[] ## blocked or non blocked per machine (true means non blocked)\n",
" # first machine\n",
" if actsitu[NM]<2: # non blocked\n",
" fm.append(True)\n",
" else:\n",
" fm.append(False)\n",
" # inside machines\n",
" for i in range(1,NM-1):\n",
" if actsitu[NM+i-1]>0 and actsitu[NM+i]<2: # non blocked\n",
" fm.append(True)\n",
" else:\n",
" fm.append(False)\n",
" # last machine\n",
" if actsitu[-1]>0: # non blocked\n",
" fm.append(True)\n",
" else:\n",
" fm.append(False)\n",
" #print(fm) \n",
"\n",
" # possible next states and effect of machines\n",
" ns=[]\n",
" nspr=[]\n",
" nsprstr=[]\n",
" movepart=[]\n",
" for i in range(NM):\n",
" if fm[i]==False:\n",
" if actsitu[i]==1:\n",
" ns.append([1])\n",
" nspr.append([1.0])\n",
" nsprstr.append([\"1.0\"]) \n",
" movepart.append([False])\n",
" else:\n",
" ns.append([0,1])\n",
" movepart.append([False,False])\n",
" nspr.append([1-r[i],r[i]])\n",
" nsprstr.append(['(1-r%d)'%(i+1),'r%d'%(i+1)])\n",
" else:\n",
" ns.append([0,1])\n",
" movepart.append([False,True])\n",
" if actsitu[i]==0:\n",
" nspr.append([1-r[i],r[i]])\n",
" nsprstr.append(['(1-r%d)'%(i+1),'r%d'%(i+1)])\n",
" else:\n",
" nspr.append([f[i],1-f[i]])\n",
" nsprstr.append(['p%d'%(i+1),'(1-p%d)'%(i+1)])\n",
" #print(ns)\n",
" #print(nspr)\n",
" #print(movepart)\n",
" \n",
" t2=tuple([len(ns[i]) for i in range(NM)])\n",
" plusneeded=False\n",
" for ind2 in ndindex(t2):\n",
" nsi=[ns[i][ind2[i]] for i in range(NM)]\n",
" nspri=prod([nspr[i][ind2[i]] for i in range(NM)])\n",
" nspristr=\"\"\n",
" for i in range(NM):\n",
" nspristr=nspristr+nsprstr[i][ind2[i]]\n",
" if i<NM-1:\n",
" nspristr=nspristr+\"*\"\n",
" for i in range(NM-1):\n",
" bl=0\n",
" if nsi[i]==1 and movepart[i][ind2[i]]==True:\n",
" bl=bl+1\n",
" if nsi[i+1]==1 and movepart[i+1][ind2[i+1]]==True:\n",
" bl=bl-1\n",
" nsi.append(bl)\n",
" # identify those that need update\n",
" update=[]\n",
" for i in range(NM):\n",
" if nsi[i]==actsitu[i]:\n",
" update.append(False)\n",
" else:\n",
" update.append(True)\n",
" for i in range(NM-1):\n",
" if nsi[i+NM]==0:\n",
" update.append(False)\n",
" else:\n",
" update.append(True)\n",
"\n",
" if plusneeded:\n",
" prismfile.write('+')\n",
" plusneeded=True\n",
" if sym:\n",
" prismfile.write('\\n %s:' % nspristr);\n",
" else:\n",
" prismfile.write('\\n %.12e:' % nspri);\n",
" \n",
" towrite=update.count(True)\n",
" if towrite==0:\n",
" prismfile.write('true')\n",
" else:\n",
" for i in range(NM):\n",
" if(update[i]):\n",
" towrite=towrite-1\n",
" prismfile.write('(m%d\\'=%d)' % (i+1,nsi[i]))\n",
" if towrite>0:\n",
" prismfile.write('&')\n",
" for i in range(NM-1):\n",
" if(update[i+NM]):\n",
" towrite=towrite-1\n",
" prismfile.write('(b%d\\'=b%d' % (i+1,i+1))\n",
" if nsi[i+NM] == -1:\n",
" prismfile.write('-1')\n",
" if nsi[i+NM] == +1:\n",
" prismfile.write('+1')\n",
" if towrite>0:\n",
" prismfile.write(')&')\n",
" else:\n",
" prismfile.write(')')\n",
" prismfile.write(';\\n')\n",
" prismfile.write(\"endmodule\\n\") \n",
" prismfile.write('\\n// THROUGHPUT\\n')\n",
" for j in range(NM):\n",
" i=j+1\n",
" if i==1:\n",
" prismfile.write('rewards \\\"throughput_M%d\\\"\\n ((m%d=1 & b%d<n%d)):1;\\nendrewards\\n' \n",
" % (i,i,i,i))\n",
" elif i==NM:\n",
" prismfile.write('rewards \\\"throughput_M%d\\\"\\n ((m%d=1 & b%d>0)):1;\\nendrewards\\n' \n",
" % (i,i,i-1))\n",
" else:\n",
" prismfile.write('rewards \\\"throughput_M%d\\\"\\n ((m%d=1 & b%d>0 & b%d<n%d)):1;\\nendrewards\\n' \n",
" % (i,i,i-1,i,i))\n",
" prismfile.close()\n",
" prismfile = open(fn+\".props\", 'w')\n",
" for j in range(NM):\n",
" prismfile.write('R{\"throughput_M%d\"}=? [ S ]\\n' % (j+1))\n",
" prismfile.close() "
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [],
"source": [
"## example with 4 machines\n",
"f=[0.01, 0.05, 0.02, 0.03]\n",
"r=[0.1, 0.2, 0.15, 0.18]\n",
"b=[8,10,6]\n",
"mi=[1,0,1,0]\n",
"bi=[2,3,4]\n",
"fn=\"4M\"\n",
"two_state_to_prism(f,r,b,mi,bi,fn,True)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.8.5"
}
},
"nbformat": 4,
"nbformat_minor": 4
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment