-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathExperiments.hs
274 lines (260 loc) · 13.3 KB
/
Experiments.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
module Experiments where
import Data.List(sort, nub)
import Data.Set(singleton)
import System.Random(mkStdGen, randomIO, randoms, randomR, randomRs)
import Control.Monad(forM_, replicateM_, when)
import Data.Time(getCurrentTime, diffUTCTime)
import System.Process(readProcess)
import Control.Concurrent(forkIO, newEmptyMVar, putMVar, takeMVar)
import Core(
Assertion(Assrt),
KripkeS(KS),
PathF(St),
bot,
evalMcALTL,
mcALTLSet,
mcALTLcSet,
mcCTLSSet,
nuXmvPath,
smvOutput
)
import RandomForms(
randomFormsCTL,
randomFormsLTL,
securityG,
vivacidadF,
fmTimesX,
progresoG,
safeG,
permGF,
repeatG,
altG,
cicloCompletoG
)
import RandomKS(randomKS, cycleKS)
import ParserNuXmv(writeNuXmv)
data TypeExperiment = LTL | LTLc | CTL deriving Eq
randomExperiment::TypeExperiment->Int->Int->Bool->IO ()
randomExperiment experiment n lforms nuXmv = do
ranInit <- randomIO
ranNumInit <- randomIO
ranKS <- randomIO
ranF <- randomIO
putStrLn $ " init seed: " ++ show ranInit
putStrLn $ " NumInit seed: " ++ show ranNumInit
putStrLn $ " KS seed: " ++ show ranKS
putStrLn $ " F seed: " ++ show ranF
seedsExperiment experiment (ranInit, ranNumInit, ranKS, ranF) n lforms nuXmv
seedsExperiment::TypeExperiment->(Int,Int,Int,Int)->Int->Int->Bool->IO ()
seedsExperiment experiment (ranInit, ranNumInit, ranKS, ranF) n lforms nuXmv =
let vars = ["p" ++ show j | j <- [0 .. n-1]] in
do
let suc_ks = randoms (mkStdGen ranKS)
k = fst $ randomR (1, 2^n) (mkStdGen ranNumInit)
inits = sort $ take k $ nub $ randomRs (0, 2^n - 1) (mkStdGen ranInit)
states = [0 .. (2^n - 1)]
ks = randomKS n suc_ks
putStrLn $ "\nKripke structure size: 2^" ++ show n
putStrLn $ "Formulas depth: " ++ show lforms
putStrLn $ "Initial states number: " ++ show k
newEmptyMVar >>= run_experiment experiment vars inits states ks
where
run_experiment exp' vars inits states ks str =
let forms = random_forms exp' in
do
print_forms forms
when nuXmv (
do
putStrLn "\n[Writing nuXmv file...]"
writeNuXmv ks states inits vars forms lforms (ranInit, ranNumInit, ranKS, ranF)
putStrLn "[nuXmv file was written]\n"
)
print_type_experiment exp'
start <- getCurrentTime
callmc exp' forms ks inits str
when (experiment /= LTLc) (replicateM_ 3 (takeMVar str >>= putStrLn))
end <- getCurrentTime
putStrLn $ "\n\tVerification time: " ++ show (diffUTCTime end start) ++ "\n"
when nuXmv nuXmvExperiment
print_forms (Left fs) = putStrLn $ "Specifications: " ++ concatMap (("\n\t• "<>) . show) fs <> "\n"
print_forms (Right fs) = putStrLn $ "Specifications: " ++ concatMap (("\n\t• "<>) . show) fs <> "\n"
callmc experiment' forms ks inits str = case experiment' of
LTL -> let Left fs = forms in
forM_ fs $ \f -> forkIO $ putMVar str $ "-- specification " ++ show f ++ " : " ++ show (mcALTLSet ks inits f)
LTLc -> let Left fs = forms in
forM_ fs (\f -> do
putStr $ "-- specification " ++ show f ++ " : "
mcALTLcSet ks inits f
)
CTL -> let Right fs = forms in
forM_ fs $ \f -> forkIO $ putMVar str $ "-- specification " ++ show f ++ " : " ++ show (mcCTLSSet (ks, inits) f)
print_type_experiment exp' = case exp' of
LTL -> putStrLn "\n\tmcALTL:\n"
LTLc -> putStrLn "\n\tmcALTLc:\n"
CTL -> putStrLn "\n\tmcCTL★:\n"
random_forms exp' = case exp' of
CTL -> Right $ sort $ randomFormsCTL lforms n ranF
_ -> Left $ sort $ randomFormsLTL lforms n ranF
nuXmvExperiment::IO ()
nuXmvExperiment = do
putStrLn "\tnuXmv:"
start <- getCurrentTime
salida_nuXmv <- readProcess nuXmvPath ["-dcx", smvOutput] []
end <- getCurrentTime
let salida_nuXmv_forms = let nuXmv_out_lines = lines salida_nuXmv
nuXmv_out = drop 26 nuXmv_out_lines in
concat [l ++ "\n" | l <- nuXmv_out]
putStrLn salida_nuXmv_forms
putStrLn $ "\tVerification time: " ++ show (diffUTCTime end start)
thesisExperiments::IO ()
thesisExperiments = do
putStrLn "\n\tLTL EXPERIMENTS\n"
putStrLn "1)"
seedsExperiment LTL (-5053428644939494458, 5533791029784639153, -7168765502673159231, -7141886416844860059) 5 2 True
putStrLn "2)"
seedsExperiment LTL (7295322385161293443, 9119911361258526469, -3976311874439943576, -8020079916767466332) 7 3 True
putStrLn "3)"
seedsExperiment LTL (-4936023892743165299, 45022348244051710, -318369156885917136, 7664302682932608404) 7 2 True
putStrLn "4)"
seedsExperiment LTL (-2600085101192994995, 5103933280507166601, 7321885015983263168, -3980215730978928173) 9 3 True
putStrLn "5)"
seedsExperiment LTL (-76398304999172336, -8563057924574850918, 5654463647766606429, 3977323623621745794) 10 3 True
putStrLn "6)"
seedsExperiment LTL (2080258398381246525, -5652026877346931720, -6901248074493425579, -5647506115212334317) 11 3 True
putStrLn "7)"
seedsExperiment LTL (-462212670351055610, -6062112136505055477, -3474006495536599128, 7263318818191457324) 12 3 False
putStrLn "8)"
seedsExperiment LTL (1210007372340279273, 6577387527259573693, 7288838695625089897, 1550804476981824494) 13 4 False
putStrLn "9)"
seedsExperiment LTL (-5513877223295918523, -1129439877177454557, -1335035135597581770, -7224920461052687264) 14 5 False
putStrLn "10)"
seedsExperiment LTL (4245131971143730679, -5160046389823251879, -2541419881106205587, 7875966796276176735) 15 3 False
putStrLn "11)"
seedsExperiment LTL (-2317318845971560383, 63174928610846957, 7740644631840446483, 6914601918853315128) 17 3 False
putStrLn "12)"
seedsExperiment LTL (57632024823226759, 6995788245303145922, 7679432384484253856, -3512037660807785758) 18 3 False
putStrLn "13)"
seedsExperiment LTL (-444226188325987799, 902136017974027903, 6074936912016031953, -1716998379019504120) 19 3 False
putStrLn "14)"
seedsExperiment LTL (124380107722107864, -2021925931603360927, 6315226998243820130, -3066682603604533009) 20 3 False
putStrLn "\tCTL EXPERIMENTS\n"
putStrLn "1)"
seedsExperiment CTL (5332018860263000951, -5659696516944381498, 6131573798985584345, 7270582556455303268) 5 3 True
putStrLn "2)"
seedsExperiment CTL (-3634750090013039070, -5400738926027436334, -4039355692805230431, -8152133867975338019) 7 3 True
putStrLn "3)"
seedsExperiment CTL (-6856179037350201869, -2206205337164536481, 410507466240855853, -1681413090854369932) 8 3 True
putStrLn "4)"
seedsExperiment CTL (8835624876428712241, 4848600760005918176, 8955329516851429801, -196645287117638075) 9 3 True
putStrLn "5)"
seedsExperiment CTL (9210208927398959434, 4419626295539301520, -8267301267196941026, 7796684326958031327) 10 3 True
putStrLn "6)"
seedsExperiment CTL (2380479831102832854, -6986691139666666669, 2195935036964894474, -8834836482381054136) 11 3 True
putStrLn "7)"
seedsExperiment CTL (2436629998256113239, -6923507982247632929, -4253175763147895628, -8973650143097053412) 12 3 True
putStrLn "8)"
seedsExperiment CTL (949953449846448731, -406275148541526948, -3842511025887463921, 4104264936417372307) 12 3 True
putStrLn "9)"
seedsExperiment CTL (100, 76, 4, 2) 12 2 True
putStrLn "10)"
seedsExperiment CTL (6237097947817666748, 7051789713999892797, 616016117592706892, 4966506196981833716) 13 2 True
putStrLn "11)"
seedsExperiment CTL (8666625547701607053, -970530960044127767, 3270900684283699943, -9112910988615369691) 15 2 False
putStrLn "12)"
seedsExperiment CTL (-5077824685923578894, 859138999552865391, 5683394313923832767, -7032287586481233253) 17 2 False
putStrLn "13)"
seedsExperiment CTL (7489358293504925504, -4212458674216479258, 2806816292527658512, -1650435001088151317) 18 2 False
putStrLn "14)"
seedsExperiment CTL (-3020335431298968450, -1085283208950323474, 7907697534437260499, 1709226432342667921) 19 2 False
putStrLn "15)"
seedsExperiment CTL (6830968738545262399, -7400582486838530919, -5225068410809829748, 4640882333315414212) 20 2 False
ltlExperiment::String->Int->String->Int->Bool->IO ()
ltlExperiment ks_type n specification m nuXmv =
if ks_type `elem` ["cycleKS", "randomKS"] && specification `elem` ["fmTimesX","securityG","vivacidadF","progresoG","safeG","permGF","repeatG","altG","cicloCompletoG"]
then do
putStrLn $ "\nEstructura de Kripke: " ++ ks_type ++ "(" ++ show n ++ ")"
let (φ_m, descr) = ltl_experiment specification
putStrLn $ "Experimento: " ++ let φ_m_s = show φ_m in
if m > 80
then take 150 φ_m_s ++ "..."
else φ_m_s
putStrLn descr
ks_n <- case ks_type of
"cycleKS" -> return $ cycleKS n
"randomKS" -> randomKS n . randoms . mkStdGen <$> randomIO
_ -> return $ KS (const [], \_ _ -> False)
when nuXmv (do
putStrLn "\n[Writing nuXmv file...]"
writeNuXmv ks_n (if ks_type == "randomKS" then [0 .. (2^n - 1)] else [0 .. n-1]) [0] ["p" ++ show j | j <- [0 .. n-1]] (Left [φ_m]) m (0, 0, 0, 0)
putStrLn "[nuXmv file was written]\n"
)
start <- getCurrentTime
putStr "\n\tmcALTL: " >> print (evalMcALTL ks_n (Assrt (0, singleton φ_m)))
end <- getCurrentTime
putStrLn $ "\n\tVerification time: " ++ show (diffUTCTime end start) ++ "\n"
when nuXmv nuXmvExperiment
else putStrLn "Tipo de KS no válido o experimento no válido"
where
ltl_experiment s = case s of
"fmTimesX" -> (
fmTimesX m,
"\n\tF(p0∧X(p1∧X(p2∧…Xpm−1)))\n\n" ++
"\tLa fórmula dice que eventualmente habrá una secuencia de 𝑚 estados consecutivos donde primero 𝑝0 es verdadero, seguido de 𝑝1, etc., hasta 𝑝𝑚−1.\n\n" ++
"\tSi 𝑚≤𝑛 la fórmula puede satisfacerse en la estructura cíclica Mn.\n" ++
"\tSi 𝑚>𝑛 la fórmula no puede satisfacerse en la estructura cíclica Mn."
)
"securityG" -> (
securityG m,
"\n\tG¬(p0∧p1∧…∧pm−1)\n\n" ++
"\tPropiedad de seguridad (ausencia de ciertos estados):\n" ++
"\tNunca habrá un estado donde todas las proposiciones 𝑝0,𝑝1,…,𝑝𝑚−1 sean verdaderas simultáneamente."
)
"vivacidadF" -> (
vivacidadF m,
"\n\tF(pn−1∧Xp0)\n\n" ++
"\tPropiedad de vivacidad (alcanzabilidad de estados específicos):\n" ++
"\tEventualmente se alcanzará el último estado etiquetado con 𝑝𝑛−1 seguido del primer estado etiquetado con 𝑝0."
)
"progresoG" -> (
progresoG m,
"\n\tφprog,n = G(p0→Fp1)∧G(p1→Fp2)∧…∧G(pn−2→Fpn−1)\n\n" ++
"\tPropiedad de Progreso:\n" ++
"\tInterpretación: Si 𝑝𝑖 es verdadero, eventualmente 𝑝𝑖+1 también será verdadero, para todos los 𝑖 en el rango de 0 a 𝑛−2\n" ++
"\tUso: Verificar que hay un progreso secuencial en el sistema, es decir, que no se queda atrapado en un estado sin avanzar."
)
"safeG" -> (
safeG m,
"\n\tφsafe,m = G¬(q0∧X(q1∧X(…Xqm−1)))\n\n" ++
"\tPropiedad de Ausencia de Secuencias Peligrosas:\n" ++
"\tInterpretación: Nunca ocurre una secuencia de 𝑚 estados consecutivos donde primero 𝑞0 es verdadero, seguido de 𝑞1, y así sucesivamente hasta 𝑞𝑚−1.\n" ++
"\tUso: Prevenir secuencias peligrosas o indeseadas de eventos en el sistema."
)
"permGF" -> (
permGF m,
"\n\tφperm,k = G(Fp0→G(p0∧X(p1∧X(…Xpk−1))))\n\n" ++
"\tPropiedad de Permanencia:\n" ++
"\tInterpretación: Si 𝑝0 es verdadero alguna vez, entonces siempre habrá una secuencia repetida de 𝑝0,𝑝1,…,𝑝𝑘−1.\n" ++
"\tUso: Asegurar que una vez alcanzado un estado particular, se mantiene una secuencia estable de eventos."
)
"repeatG" -> (
repeatG m,
"\n\tφrepeat,n = G(p0→F(p1∧F(p2∧…Fpn−1)))\n\n" ++
"\tPropiedad de Repetición Periódica:\n" ++
"\tInterpretación: Si 𝑝0 es verdadero, entonces eventualmente ocurrirá 𝑝1, seguido de 𝑝2, y así sucesivamente hasta 𝑝𝑛−1, repetidamente.\n" ++
"\tUso: Verificar que una secuencia de eventos ocurre de forma cíclica o periódica."
)
"altG" -> (
altG m,
"\n\tφalt,m = G(p0→(Fp1∨Fp2∨…∨Fpm−1))\n\n" ++
"\tPropiedad de Alternancia:\n" ++
"\tInterpretación: Si 𝑝0 es verdadero, eventualmente uno de 𝑝1,𝑝2,…,𝑝𝑚−1 será verdadero.\n" ++
"\tUso: Especificar que después de un evento inicial, al menos una de varias opciones posibles debe ocurrir."
)
"cicloCompletoG" -> (
cicloCompletoG m,
"\n\tφcycle,n = G((p0∧Xp1∧…∧X^(n−1)pn−1)→X^np0\n\n" ++
"\tPropiedad de Alternancia:\n" ++
"\tInterpretación: Después de una secuencia completa de 𝑝0,𝑝1,…,𝑝𝑛−1, el ciclo se repite desde 𝑝0.\n" ++
"\tUso: Modelar ciclos completos de eventos que se repiten indefinidamente."
)
_ -> (St bot, "")