Formal modeling and simulation for SARS-CoV-2 containment scenarios in Catalonia

0123456789  !"#  $%&'()*+&,*-./+'0*&)12+03(*2/,1 456789:;6<=:>?@9?<A>8B:9C>6?D67AEFAG HI6JGKI6?C9>?8=?CAL=?97>6M>?I9C9:6?>9 N OPQRSTUVWX 3YXUXU Z[Q\X]W^X37_`^]XTXZXTabQ\X]WcX3YX]]XUWSZdefghijfklkmnofk p hqefqlrhslkloteulvwxwyzv {|liqhonelv }~lfe QP^3PXS  VUZdefghijfklkhiklrhslkloteulvwxwxv|liqhonelv}~lfe 0 \X`]^VX ^TV]Zsliohknedefghijfkuvkkllvv}|vslelrl 00 hrhe hfekhiiholkhrnrhojknjftolkhkhj~ihlrn}}snfeslkloneflv 0 fqql ehtjhrknhhqkfghoutforjftolkfnel~~ofqlkfnejlerlelouhkh 0$ hhqkjn ene~lilqhtkfqlofekhighekfnejthknkhqnejklekhgnotkfnenkfj 04 ~lerh fqvlerkhehhrknklhltokfrfjqf~ofeliul~~inlqvhtjhlnilo 0H j~hqfql kfneknih~ihjhekkhnrholerknglofrlkhkhnrholjjt~kfnejh 0N rfjqtjj khrhefkfnenkhnrhotjfenilooletlhjvlerkh}~hqfqlkfne 0O lerhj qif~kfneletlhknf~inghqntefqlkfnehkhhejklhnorhijh 0{ jnni loflkfnerhklfojvrfjqtjjf~ofqlkfnejfekhglofrlkfne~inqhjjvler 0 ~ihjhek nihjtokjnklfehrinkhnrhonkh~lerhfqfeslkloneflqleh  tjhrni rhqfjfnelfe 0   ¡ ¡ ¢     £ $ ¡    ¢¡# 4 ¤ ¥ ¡£ H ¡ ¡ #  N ¡  ¦ O   §¡¨ {  !©£ª«£¬£   # ¨¡ $ ¨ ¨¨¡¥£ $0  #  ¨ ¨¨£ $    ª  ! $$  !¡¡¨ $4 ¡   #   $H   ®¯°± ® ¥¡¡  $N  ¡8 ¡¡£ $O ²³´µ¶ ·¸¹º»¶¨¼½¾¶µ¸¶¿¡£ ${  À¶ÁÂö¿¨¡¡  $  Ä 4ÅÆ¡²¼À£ 40  ¨# 4¡   Ç 4$©#8ȶµ¶É´¶¿ 44À¶µÂöʶ¿Ë Ìͷ´¶¿¡£ 4H¡¢¡ 4NÄ¡Å 4O¥¨ªË«§£®¯¡ 4{¡ ¡  4#¨ H  ¥ ¡£ H0  ¦ H¨¡ ÄÆÎÅ H$!#   H4# # £# Ï HH  ¢¡ ¡ HN¨ HO¡¨¨¢¡ H{¨¨¨¨¥¨¢¡ H#  ¨ N¨ N0¨#¡ ¡ N¡# ¢ "¡ N$  ¨  ¡ N4  ¨  ®Ð¬®£¯Ñ®ÐÒ ¬±¬¬ÓÓÓ § ËÔÕ®±®®±¯ÖתÓ¬±¬¬°®ØѬ¬Ù ÚÛÚÚÜÝÞßàáâãäÞåæâãçèèèéêëìÝæãíîêïàãæåéêëìÝæàðñàðîïàãðïãòèðñàðããíàðñ ó 01 23453 6787973259847576287346673892 00 845 45385647622845387327 0 487 59764325784875469284524887 0 72 7772474926452284525 0 763 284587357 !377675894784 " 964 7766467873845 4845758452597 # 97582 845$!77578677947828676775887 % 297 &879!87675887357847787 ' 678 267926 24!58778738454766467 ( 3495 786779478284345767582738 1 487 94725325774636422845 0 78!77 5877947 5367253678&487  46732 8259&5766467873845  )*+,* -.  /76 8947 77550671223245678 9 64848&7 " 757 54&8798&52932483254374587 # 252& 487728&487:7&298457& % 87 767587;7686878475678282925 ' 2738 26782:75584345762845 467;297 87 ( 3494 84548742845 8752867487349 1 26897 5884774587947 2587582262 0 9786<2 84546874=744>672/774845  425 573875243787? 5;47?  657384 ? 7734767468725233492689758  67677 58278487428455828733 " 82872 58794748725793747&862576 # 655 2649457349268975884254876467 % 2253 7764548748947537487637526 ' 4 :7 34557975828&252286494 ( 378 78445572524!525252&487 1 8794 62748454872579346723!273/ 0 947 475487672282 88784252&<787  679 526&94729845  @ABC,D +,*-.  /77 345947 85E&845 78748 #"" 947 86386725489<7258874767 #"# 282 52928725572524689> 2 /7 #"% 4F738 7844825872629787657774687 #"' 869 47/7489<28459477874767 #"( 3272 25582586784523678288!8 #"1 877 4762845287972547752&3/ #"0 947 2874F738748&587748454 #" 327 5282452847572238625945628784 #" 77 58748G9477789287776226297 #" 87646 8767254876 5358777387 ##" 6764 3875976H I !37849726787 ### :7&8 625945487727H I 676775887 ##%2762759764734526&5738456437&2 ##'575738452H I J1 8759764327! ##(536727 25H I K1 8759764327!7367273 ##1LE627 673587948&48742845 46 ##09252858774292:3273887274H I M6 ##94778928787/6259457287N2!3 ##7275884H I 3232872O P QRS!8673476& ##6287S3N3232875476728282858 #%"878446E&845947 489<52588587 #%#4767282732558786754874767 #%%327 25!758786753257246582537 #%'7327457!587675845:7233573 !7 325 #%(34987257!N27 #%1=88458 !8879252984592725 #%087:7&26297876323287 !7286947 #%828537287577729845467345 #%92:525828278464724673282745 #%84632282257;768:54!77 #'")*.+,*-. #'#/7289478547332845258736 #'%845G2527248G3 > !36472469225 #''5294973259847367672!46& #'(879 T /748G94724!842782729 #'1845257246!75LE6267274657! #'0:54!772488766722227M68729 #'774722678&4764548748G 7234!3 #'537872984546875876758452728 #'87897487252&/42287886947 !7 #("349267872&57!327467328!8228278 #(#828345825872&57!3275282452  #(%48G262324F7384675872527!8 #('52944692792583 82526<7&87 #((65876528452/773499532845U54548G7 #(1467626332543:$134V4/5 >3WGMX #(0T3E7M544 2593E7M58U754/74V4/525 #(WGMX2629 676775887947Y863867 #(52762633273494845E7M54425 #(E7M58U75475787947Y7246WGMX #1"25E7M544267=Z5L/4828782873499 #1#532845 75546ZL=G4864[=LL5G4 #1%46ZL=G453845228676 7576285877;73 #1'845427842384552E7M544/46767758 #1(897 246ZL=G44!5 2 72&2629787625267 #114687&72&256468&58758774776& #1058325574V4/587849482629525& #148G947 6767758587925779758487 #1863867487947 #10671234!8794778446732887 #0"734525793!275282452/72629 2 05 87E&84594758747M3725763728874 4!5U7G$88ÿ$]]446]1^>99TT]M_`Ta`T>1  88ÿ$]]4765476875328328]75]27b47687] cdefghijkljkmnjoknopqkljkoorjkl stss uvwxyz{|}~wyz~v} 0123456 789999999 !8" #$## %&'()*+,-+,./+0,/012,-+,003+,- 4 56789:;<=>79?@:>6A= 010 2342353 675783939923367 01 7783 93363323267825783 01 523 5234235367783!!32367"4273675!783 01# 9$% 3&'()96783936*335 01+ !2783 93,-3"42378377835. 011 747 5!276/783934235644201 012 76 7783463".53763837839 014 3 423523373657632576 015 7833!! 3"75!78367$5 028 $!6 33323'()9"63367839 020 3 76"3633382&!26576"3""673 02 6 53"35367832"73235,8353633 02 '() 9!78393239,:;<=>=?@?=A234231 02# 53676 78344766"663367787"667 02+ 3" 330453BC,:D=E?FAGH?I?A?FA?J783424276 021 !6!3 "7365373"73556787373"1 022 76 42353273BK,:;<=ALG=@?=AMFAG<=N"61 024 72578 367$"7657O36*7837827357423367 025 783542 3!9P%91(Q1C 048 83 9356"35"32776 040 &(P, R 638"83"8"323423536757835423! 04 9P%91( Q1C323"8!(76.5S378%365 04 85 35767833.5554765*"1 04# 426 783235753787837!23"88378236 04+ TUVWXY TZXWTW[\]\YU[ ][V 041 ^]XY_`] \YU[ 042 4 33677839353353979 " "1 044 47325 !7323787"6303"7396Q935 045  76""273235757833558631 058 76378 357642373256"6783a423732 050 5"55 33232737732423"77835423!78325 05 !23 "577833!a2678353"6337783 05 5727 !7835"8*326bCcCc3353"6 05#4773265!667832"67235787572737835"8 05+*3232325"85978)23&P57CRCcCc,6 051$523&93473329CcCc,d56783231327!2 0527853"67235334437837*78647e763 0547367!*78537467538323783a3"863 05583533323"223733783"8!78367$54764"3 88835763787833!78353"6336 80(76366f62*CgCcCc-787832536 8"53567832"89RCcCc"O3635443 8 &30"347!235536732O325,P254"335"536 8#7832"8CK-83678357764236783P42 8+9K78332O325!783657253"72237263732O 816783P42Cc7833263674235"5O57 8275"7e365$6783!36678578323572"7653323 842*!7367f*CcCcP778546733""73 85633a7234235367"86367835423!78325 08567836*556367837!2$523653 00783"736"36"36(766$523-35 0"65323787783632553232678351 0 3236"235337883233!"77*6 0#"67"76787783*3673532786783 0+632576326783"O3678324231 0173253323783373"7627367835*477"441 0276 h b23C5835783!23"57!2633"535 04423"7356!!323675"3625 0583!23"576353545777i57783 842373257""73783376"23!633"535 0$67832378357O3*577655836623 637878325"3625787234235367355O3*571  765856*55!!!323674765356325 #7632576783!723376!783463"6 +O36!233"5658323636783235835 1783!23"5757""3473*78363043275"61 25326355476568*47835358351 4763632735732673578343"561O325 5 3836"65326!!3236767$5&5335322256783  8 304323678*4783535,$!26783376!783 jklm nopqb23"57!26336!3"765/23639378325"3625378!!323678*4783535 " 877ÿ45/ss545"s tuvwxyz{|}{|~{||}{|{|}   012 34567895 7449476448697379783994 010 77 345678997769775769775 011 756957 557745773769 01 4 9574794577668495 01 737956 799584 95 01! "79 46446 6 95695#7$78457 01% &5694 '#$&(456786774995 01) 95 496476449574644'954*595 01+ ,9 54964954334("757867 0- 97954 967'97767746977577 02 77578 67.7445674644987797(7 00 77447 7377456749477867 01 9396 74479584955674567 0 4745 79573456789.795943 0 37575 95757/$&474339767 0! 3456789 0% 012034561 2 0) 76759 95867456439633959737 0+ 94983 45673746697479 7 0- *78&9:; 476,<=,*8>,98495867 02 4969 5?@ABCDE75498347739 00 7756 734567897954765734 01 73967896 44"7769646457686 0 7983 77379695874557 0 8486 77785676'9574837 0! 477 77476867(4459579 0% 495456 496495786775576448 0) 778 5676787 449477 0+ 867'95 ,9(456745674969 0!- 7959944 8395456754773746 0!2 769747 F4756867'95$5(4695 0!0 7783 47497375875545679 0!1 847734 48777867796867'9 0! 95,9G(9 76567456795H757/$&5 0! 7334 9545637877478954 0!! 957 778673967496874598 0!% 49647 7I4978674567384 7679 0!) 95456 6795H757/$&7784 0!+ 867958 76737757789837 0%- 88594 959737456454973 0%2 7797 39695487459885995456 0%0 595 496495983956799584 95 0%1 J0K21L 3M NOPM2Q5 0% 9  43376**9567R45>S>SGS:T 0% 74 69 745 95G4U&V49457 0%! 973 W7.468959495 0%% XMYMXM20M5 0%):=<5675Z7#784 [\#7569 7396789 0%+76778]^_``abAB@a^Dc`aTd33d[d> 0)-:;;:69e:S:S:fg,SS;>h>iS'ST(hSSd;i 0)2>j,74&77jR4695$U574&*44456U 0)0#9775Z,9Gk7&4547]lmBanopqcr_sa 0)1;df;33>t[i:>S:T 0)duG794$U574&*44456u74 v 54Z\6795 0)457794456349959459954*9745394 0)!93794954566793954547]nDs_`ABDcm 0)%h;33:S>S[:SdT>S:d69e:S::ttgSSdtTi;t:di;Tti> 0))ij855 456="97wmlmBrcx_yBDcmBclmEzyBDc_{ 0)+oD{zA{zbcxz``Dm|76}#e76}59$7>S:S 0+-T$U574&*44uR494&,94548R494& 0+2*44uG,9467V47u=84456~$9 0+0Z,9G744845*78&9:;57349495] 0+195rcyaB@n{BawmA`abcxz`a>S>S33:ii[:Td 0+f/994zBA`aZj98495748384949 0+5754995795'*78&9:;(]lmBaalmEzyBaoD{a 0+!;i33:Ti[:TT>S>S69e:S:S:fgW9W96>S>SSdS>S 0+%94374$759}5979 0+)*44594'}$*(95776984956443795 0++37495774456499,957>S:t794878 1--7788977iS77595779595695*44 1-2594*5498434376 1-094374$759}5979 1-1*44594'}$*(456}5979467V4754957,499 1-456737495=77497348759574:S74 1-7379757953W7747686795456984953W 1-!7*54984W454949454376 1-% 779767847.677795 1-)83745643397639734993479598495 1-+456867953W795$7647443&54 12-U&V4564j*/&77577$759}5979*4 1224594*54984949437647 120 747957\475&56iS4}$* 1214747375}5979*445947779767\, 1267779595694759577958$759}5979 12*44594'}$*(*54984397595757 12!9437979734875, 12%78 456*837j5957795*475}5979 12)7447/*454647947,*,7,97 12+\6795456,98495&5754954*54984 10-495774754 6 ÿ3egg3456638  ¡¢£¤¥¦§¨¦§©ª¦«§ª«¬§¨¦§««®¦§¨ ¯ °±²³´µ¶·¸¹²´º»µ¹±¼¸