Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Bentriou Mahmoud
MarkovProcesses.jl
Commits
48a39408
Commit
48a39408
authored
Dec 03, 2020
by
Bentriou Mahmoud
Browse files
Renaming of fields for more readability
parent
21f736b8
Changes
12
Hide whitespace changes
Inline
Side-by-side
automata/automaton_F.jl
View file @
48a39408
...
...
@@ -2,7 +2,7 @@
function
create_automaton_F
(
m
::
ContinuousTimeModel
,
x1
::
Float64
,
x2
::
Float64
,
t1
::
Float64
,
t2
::
Float64
,
str_obs
::
String
)
@assert
str_obs
in
m
.
g
# Locations
l
_l
oc
=
[
"l0"
,
"l1"
,
"l2"
,
"l3"
]
loc
ations
=
[
"l0"
,
"l1"
,
"l2"
,
"l3"
]
## Invariant predicates
true_inv_predicate
=
(
A
::
LHA
,
S
::
StateLHA
)
->
return
true
...
...
@@ -10,17 +10,17 @@ function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
"l2"
=>
true_inv_predicate
,
"l3"
=>
true_inv_predicate
)
## Init and final loc
l
_l
oc_init
=
[
"l0"
]
l
_l
oc_final
=
[
"l2"
]
loc
ations
_init
=
[
"l0"
]
loc
ations
_final
=
[
"l2"
]
#S.n <=> S.
l_var
[A.map_var_automaton_idx["n"]]
#P <=> xn[map_var_model_idx[
l_cte
s[str_O]] with str_O = "P". On stock str_O dans
l_cte
s
#S.n <=> S.
values
[A.map_var_automaton_idx["n"]]
#P <=> xn[map_var_model_idx[
constant
s[str_O]] with str_O = "P". On stock str_O dans
constant
s
# P = get_value(A, x, str_obs)
## Map of automaton variables
map_var_automaton_idx
=
Dict
{
VariableAutomaton
,
Int
}(
"n"
=>
1
,
"d"
=>
2
,
"isabs"
=>
3
)
## Flow of variables
l_
flow
=
Dict
{
VariableAutomaton
,
Vector
{
Float64
}}(
"l0"
=>
[
0.0
,
0.0
,
0.0
],
flow
=
Dict
{
VariableAutomaton
,
Vector
{
Float64
}}(
"l0"
=>
[
0.0
,
0.0
,
0.0
],
"l1"
=>
[
0.0
,
0.0
,
0.0
],
"l2"
=>
[
0.0
,
0.0
,
0.0
],
"l3"
=>
[
0.0
,
0.0
,
0.0
])
...
...
@@ -45,8 +45,8 @@ function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
# l1 loc : we construct the edges of the form l1 => (..)
tuple
=
(
"l1"
,
"l2"
)
cc_aut_F_l1l2_1
(
A
::
LHA
,
S
::
StateLHA
)
=
(
A
.
l_cte
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
l_cte
s
[
"x2"
])
&&
(
A
.
l_cte
s
[
"t1"
]
<=
S
.
time
<=
A
.
l_cte
s
[
"t2"
])
(
A
.
constant
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
constant
s
[
"x2"
])
&&
(
A
.
constant
s
[
"t1"
]
<=
S
.
time
<=
A
.
constant
s
[
"t2"
])
us_aut_F_l1l2_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
;
S
[
"d"
]
=
0
)
...
...
@@ -54,14 +54,14 @@ function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
cc_aut_F_l1l2_2
(
A
::
LHA
,
S
::
StateLHA
)
=
S
[
"d"
]
>
0
&&
(
S
.
time
>
A
.
l_cte
s
[
"t2"
]
||
istrue
(
S
[
"isabs"
]))
(
S
.
time
>
A
.
constant
s
[
"t2"
]
||
istrue
(
S
[
"isabs"
]))
us_aut_F_l1l2_2!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
)
edge2
=
Edge
([
nothing
],
cc_aut_F_l1l2_2
,
us_aut_F_l1l2_2!
)
cc_aut_F_l1l2_3
(
A
::
LHA
,
S
::
StateLHA
)
=
S
[
"d"
]
==
0
&&
S
.
time
>=
A
.
l_cte
s
[
"t1"
]
S
.
time
>=
A
.
constant
s
[
"t1"
]
us_aut_F_l1l2_3!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
)
edge3
=
Edge
([
nothing
],
cc_aut_F_l1l2_3
,
us_aut_F_l1l2_3!
)
...
...
@@ -70,27 +70,27 @@ function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
tuple
=
(
"l1"
,
"l3"
)
cc_aut_F_l1l3_1
(
A
::
LHA
,
S
::
StateLHA
)
=
(
A
.
l_cte
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
l_cte
s
[
"x2"
])
(
A
.
constant
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
constant
s
[
"x2"
])
us_aut_F_l1l3_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l3"
;
S
[
"d"
]
=
0
;)
edge1
=
Edge
([
nothing
],
cc_aut_F_l1l3_1
,
us_aut_F_l1l3_1!
)
cc_aut_F_l1l3_2
(
A
::
LHA
,
S
::
StateLHA
)
=
(
S
[
"n"
]
<
A
.
l_cte
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
l_cte
s
[
"x2"
])
&&
(
S
.
time
<=
A
.
l_cte
s
[
"t1"
])
(
S
[
"n"
]
<
A
.
constant
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
constant
s
[
"x2"
])
&&
(
S
.
time
<=
A
.
constant
s
[
"t1"
])
us_aut_F_l1l3_2!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l3"
;
S
[
"d"
]
=
min
(
sqrt
((
S
.
time
-
A
.
l_cte
s
[
"t1"
])
^
2
+
(
S
[
"n"
]
-
A
.
l_cte
s
[
"x2"
])
^
2
),
sqrt
((
S
.
time
-
A
.
l_cte
s
[
"t1"
])
^
2
+
(
S
[
"n"
]
-
A
.
l_cte
s
[
"x1"
])
^
2
)))
S
[
"d"
]
=
min
(
sqrt
((
S
.
time
-
A
.
constant
s
[
"t1"
])
^
2
+
(
S
[
"n"
]
-
A
.
constant
s
[
"x2"
])
^
2
),
sqrt
((
S
.
time
-
A
.
constant
s
[
"t1"
])
^
2
+
(
S
[
"n"
]
-
A
.
constant
s
[
"x1"
])
^
2
)))
edge2
=
Edge
([
nothing
],
cc_aut_F_l1l3_2
,
us_aut_F_l1l3_2!
)
cc_aut_F_l1l3_3
(
A
::
LHA
,
S
::
StateLHA
)
=
(
S
[
"n"
]
<
A
.
l_cte
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
l_cte
s
[
"x2"
])
&&
(
A
.
l_cte
s
[
"t1"
]
<=
S
.
time
<=
A
.
l_cte
s
[
"t2"
])
(
S
[
"n"
]
<
A
.
constant
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
constant
s
[
"x2"
])
&&
(
A
.
constant
s
[
"t1"
]
<=
S
.
time
<=
A
.
constant
s
[
"t2"
])
us_aut_F_l1l3_3!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l3"
;
S
[
"d"
]
=
min
(
S
[
"d"
],
min
(
abs
(
S
[
"n"
]
-
A
.
l_cte
s
[
"x1"
]),
abs
(
S
[
"n"
]
-
A
.
l_cte
s
[
"x2"
]))))
S
[
"d"
]
=
min
(
S
[
"d"
],
min
(
abs
(
S
[
"n"
]
-
A
.
constant
s
[
"x1"
]),
abs
(
S
[
"n"
]
-
A
.
constant
s
[
"x2"
]))))
edge3
=
Edge
([
nothing
],
cc_aut_F_l1l3_3
,
us_aut_F_l1l3_3!
)
map_edges
[
tuple
]
=
[
edge1
,
edge2
,
edge3
]
...
...
@@ -104,17 +104,17 @@ function create_automaton_F(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
edge1
=
Edge
([
"ALL"
],
cc_aut_F_l3l1_1
,
us_aut_F_l3l1_1!
)
tuple
=
(
"l3"
,
"l2"
)
cc_aut_F_l3l2_1
(
A
::
LHA
,
S
::
StateLHA
)
=
(
S
.
time
>=
A
.
l_cte
s
[
"t2"
])
(
S
.
time
>=
A
.
constant
s
[
"t2"
])
us_aut_F_l3l2_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
)
edge2
=
Edge
([
nothing
],
cc_aut_F_l3l2_1
,
us_aut_F_l3l2_1!
)
map_edges
[
tuple
]
=
[
edge1
,
edge2
]
## Constants
l_cte
s
=
Dict
{
String
,
Float64
}(
"x1"
=>
x1
,
"x2"
=>
x2
,
"t1"
=>
t1
,
"t2"
=>
t2
)
constant
s
=
Dict
{
String
,
Float64
}(
"x1"
=>
x1
,
"x2"
=>
x2
,
"t1"
=>
t1
,
"t2"
=>
t2
)
A
=
LHA
(
m
.
l_
transitions
,
l
_loc
,
Λ_F
,
l_loc
_init
,
l_
loc_final
,
map_var_automaton_idx
,
l_
flow
,
map_edges
,
l_cte
s
,
m
.
map_var_idx
)
A
=
LHA
(
m
.
transitions
,
l
ocations
,
Λ_F
,
locations
_init
,
loc
ations
_final
,
map_var_automaton_idx
,
flow
,
map_edges
,
constant
s
,
m
.
map_var_idx
)
return
A
end
...
...
automata/automaton_G.jl
View file @
48a39408
...
...
@@ -2,7 +2,7 @@
function
create_automaton_G
(
m
::
ContinuousTimeModel
,
x1
::
Float64
,
x2
::
Float64
,
t1
::
Float64
,
t2
::
Float64
,
str_obs
::
String
)
@assert
str_obs
in
m
.
g
# Locations
l
_l
oc
=
[
"l0"
,
"l1"
,
"l2"
,
"l3"
,
"l4"
]
loc
ations
=
[
"l0"
,
"l1"
,
"l2"
,
"l3"
,
"l4"
]
# Invariant predicates
true_inv_predicate
=
(
A
::
LHA
,
S
::
StateLHA
)
->
return
true
...
...
@@ -11,15 +11,15 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
"l4"
=>
true_inv_predicate
)
## Init and final loc
l
_l
oc_init
=
[
"l0"
]
l
_l
oc_final
=
[
"l2"
]
loc
ations
_init
=
[
"l0"
]
loc
ations
_final
=
[
"l2"
]
## Map of automaton variables
map_var_automaton_idx
=
Dict
{
VariableAutomaton
,
Int
}(
"tprime"
=>
1
,
"in"
=>
2
,
"n"
=>
3
,
"d"
=>
4
,
"isabs"
=>
5
)
## Flow of variables
l_
flow
=
Dict
{
VariableAutomaton
,
Vector
{
Float64
}}(
"l0"
=>
[
0.0
,
0.0
,
0.0
,
0.0
,
0.0
],
flow
=
Dict
{
VariableAutomaton
,
Vector
{
Float64
}}(
"l0"
=>
[
0.0
,
0.0
,
0.0
,
0.0
,
0.0
],
"l1"
=>
[
0.0
,
0.0
,
0.0
,
0.0
,
0.0
],
"l2"
=>
[
0.0
,
0.0
,
0.0
,
0.0
,
0.0
],
"l3"
=>
[
0.0
,
0.0
,
0.0
,
0.0
,
0.0
],
...
...
@@ -45,27 +45,27 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
# l1 loc
tuple
=
(
"l1"
,
"l3"
)
cc_aut_G_l1l3_1
(
A
::
LHA
,
S
::
StateLHA
)
=
S
.
time
<=
A
.
l_cte
s
[
"t1"
]
&&
S
[
"n"
]
<
A
.
l_cte
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
l_cte
s
[
"x2"
]
S
.
time
<=
A
.
constant
s
[
"t1"
]
&&
S
[
"n"
]
<
A
.
constant
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
constant
s
[
"x2"
]
us_aut_G_l1l3_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l3"
;
S
[
"d"
]
=
min
(
abs
(
A
.
l_cte
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
l_cte
s
[
"x2"
]
-
S
[
"n"
]));
S
[
"d"
]
=
min
(
abs
(
A
.
constant
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
constant
s
[
"x2"
]
-
S
[
"n"
]));
S
[
"in"
]
=
false
)
edge1
=
Edge
([
nothing
],
cc_aut_G_l1l3_1
,
us_aut_G_l1l3_1!
)
cc_aut_G_l1l3_3
(
A
::
LHA
,
S
::
StateLHA
)
=
!
istrue
(
S
[
"in"
])
&&
(
A
.
l_cte
s
[
"t1"
]
<=
S
.
time
<=
A
.
l_cte
s
[
"t2"
])
&&
(
A
.
l_cte
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
l_cte
s
[
"x2"
])
(
A
.
constant
s
[
"t1"
]
<=
S
.
time
<=
A
.
constant
s
[
"t2"
])
&&
(
A
.
constant
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
constant
s
[
"x2"
])
us_aut_G_l1l3_3!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l3"
;
S
[
"d"
]
=
S
[
"d"
]
*
(
S
.
time
-
A
.
l_cte
s
[
"t1"
]);
S
[
"d"
]
=
S
[
"d"
]
*
(
S
.
time
-
A
.
constant
s
[
"t1"
]);
S
[
"tprime"
]
=
0.0
)
edge3
=
Edge
([
nothing
],
cc_aut_G_l1l3_3
,
us_aut_G_l1l3_3!
)
cc_aut_G_l1l3_2
(
A
::
LHA
,
S
::
StateLHA
)
=
(
S
.
time
<=
A
.
l_cte
s
[
"t1"
])
&&
(
A
.
l_cte
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
l_cte
s
[
"x2"
])
(
S
.
time
<=
A
.
constant
s
[
"t1"
])
&&
(
A
.
constant
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
constant
s
[
"x2"
])
us_aut_G_l1l3_2!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l3"
;
S
[
"d"
]
=
0
;
...
...
@@ -74,8 +74,8 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
cc_aut_G_l1l3_4
(
A
::
LHA
,
S
::
StateLHA
)
=
istrue
(
S
[
"in"
])
&&
(
A
.
l_cte
s
[
"t1"
]
<=
S
.
time
<=
A
.
l_cte
s
[
"t2"
])
&&
(
A
.
l_cte
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
l_cte
s
[
"x2"
])
(
A
.
constant
s
[
"t1"
]
<=
S
.
time
<=
A
.
constant
s
[
"t2"
])
&&
(
A
.
constant
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
constant
s
[
"x2"
])
us_aut_G_l1l3_4!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l3"
;
S
[
"tprime"
]
=
0.0
)
...
...
@@ -86,16 +86,16 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
tuple
=
(
"l1"
,
"l4"
)
cc_aut_G_l1l4_1
(
A
::
LHA
,
S
::
StateLHA
)
=
!
istrue
(
S
[
"in"
])
&&
(
A
.
l_cte
s
[
"t1"
]
<=
S
.
time
<=
A
.
l_cte
s
[
"t2"
])
&&
(
S
[
"n"
]
<
A
.
l_cte
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
l_cte
s
[
"x2"
])
(
A
.
constant
s
[
"t1"
]
<=
S
.
time
<=
A
.
constant
s
[
"t2"
])
&&
(
S
[
"n"
]
<
A
.
constant
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
constant
s
[
"x2"
])
us_aut_G_l1l4_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l4"
;
S
[
"d"
]
+=
S
[
"d"
]
*
(
S
.
time
-
A
.
l_cte
s
[
"t1"
]))
S
[
"d"
]
+=
S
[
"d"
]
*
(
S
.
time
-
A
.
constant
s
[
"t1"
]))
edge1
=
Edge
([
nothing
],
cc_aut_G_l1l4_1
,
us_aut_G_l1l4_1!
)
cc_aut_G_l1l4_2
(
A
::
LHA
,
S
::
StateLHA
)
=
istrue
(
S
[
"in"
])
&&
(
A
.
l_cte
s
[
"t1"
]
<=
S
.
time
<=
A
.
l_cte
s
[
"t2"
])
&&
(
S
[
"n"
]
<
A
.
l_cte
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
l_cte
s
[
"x2"
])
(
A
.
constant
s
[
"t1"
]
<=
S
.
time
<=
A
.
constant
s
[
"t2"
])
&&
(
S
[
"n"
]
<
A
.
constant
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
constant
s
[
"x2"
])
us_aut_G_l1l4_2!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l4"
)
edge2
=
Edge
([
nothing
],
cc_aut_G_l1l4_2
,
us_aut_G_l1l4_2!
)
...
...
@@ -104,31 +104,31 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
tuple
=
(
"l1"
,
"l2"
)
cc_aut_G_l1l2_1
(
A
::
LHA
,
S
::
StateLHA
)
=
istrue
(
S
[
"in"
])
&&
S
.
time
>=
A
.
l_cte
s
[
"t2"
]
S
.
time
>=
A
.
constant
s
[
"t2"
]
us_aut_G_l1l2_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
)
edge1
=
Edge
([
nothing
],
cc_aut_G_l1l2_1
,
us_aut_G_l1l2_1!
)
cc_aut_G_l1l2_2
(
A
::
LHA
,
S
::
StateLHA
)
=
!
istrue
(
S
[
"in"
])
&&
S
.
time
>=
A
.
l_cte
s
[
"t2"
]
S
.
time
>=
A
.
constant
s
[
"t2"
]
us_aut_G_l1l2_2!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
;
S
[
"d"
]
=
S
[
"d"
]
*
(
A
.
l_cte
s
[
"t2"
]
-
A
.
l_cte
s
[
"t1"
]))
S
[
"d"
]
=
S
[
"d"
]
*
(
A
.
constant
s
[
"t2"
]
-
A
.
constant
s
[
"t1"
]))
edge2
=
Edge
([
nothing
],
cc_aut_G_l1l2_2
,
us_aut_G_l1l2_2!
)
cc_aut_G_l1l2_3
(
A
::
LHA
,
S
::
StateLHA
)
=
istrue
(
S
[
"isabs"
])
&&
S
.
time
<=
A
.
l_cte
s
[
"t1"
]
S
.
time
<=
A
.
constant
s
[
"t1"
]
us_aut_G_l1l2_3!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
;
S
[
"d"
]
=
S
[
"d"
]
*
(
A
.
l_cte
s
[
"t2"
]
-
A
.
l_cte
s
[
"t1"
]))
S
[
"d"
]
=
S
[
"d"
]
*
(
A
.
constant
s
[
"t2"
]
-
A
.
constant
s
[
"t1"
]))
edge3
=
Edge
([
nothing
],
cc_aut_G_l1l2_3
,
us_aut_G_l1l2_3!
)
cc_aut_G_l1l2_4
(
A
::
LHA
,
S
::
StateLHA
)
=
istrue
(
S
[
"isabs"
])
&&
(
A
.
l_cte
s
[
"t1"
]
<=
S
.
time
<=
A
.
l_cte
s
[
"t2"
])
(
A
.
constant
s
[
"t1"
]
<=
S
.
time
<=
A
.
constant
s
[
"t2"
])
us_aut_G_l1l2_4!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
;
S
[
"d"
]
+=
(
A
.
l_cte
s
[
"t2"
]
-
S
.
time
)
*
min
(
abs
(
A
.
l_cte
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
l_cte
s
[
"x1"
]
-
S
[
"n"
])))
S
[
"d"
]
+=
(
A
.
constant
s
[
"t2"
]
-
S
.
time
)
*
min
(
abs
(
A
.
constant
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
constant
s
[
"x1"
]
-
S
[
"n"
])))
edge4
=
Edge
([
nothing
],
cc_aut_G_l1l2_4
,
us_aut_G_l1l2_4!
)
map_edges
[
tuple
]
=
[
edge1
,
edge2
,
edge3
,
edge4
]
...
...
@@ -146,14 +146,14 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
tuple
=
(
"l3"
,
"l2"
)
cc_aut_G_l3l2_2
(
A
::
LHA
,
S
::
StateLHA
)
=
istrue
(
S
[
"in"
])
&&
S
.
time
>=
A
.
l_cte
s
[
"t2"
]
S
.
time
>=
A
.
constant
s
[
"t2"
]
us_aut_G_l3l2_2!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
;
S
[
"d"
]
=
S
[
"d"
]
*
(
A
.
l_cte
s
[
"t2"
]
-
A
.
l_cte
s
[
"t1"
]))
S
[
"d"
]
=
S
[
"d"
]
*
(
A
.
constant
s
[
"t2"
]
-
A
.
constant
s
[
"t1"
]))
edge2
=
Edge
([
nothing
],
cc_aut_G_l3l2_2
,
us_aut_G_l3l2_2!
)
cc_aut_G_l3l2_1
(
A
::
LHA
,
S
::
StateLHA
)
=
!
istrue
(
S
[
"in"
])
&&
S
.
time
>=
A
.
l_cte
s
[
"t2"
]
S
.
time
>=
A
.
constant
s
[
"t2"
]
us_aut_G_l3l2_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
)
edge1
=
Edge
([
nothing
],
cc_aut_G_l3l2_1
,
us_aut_G_l3l2_1!
)
...
...
@@ -165,7 +165,7 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
cc_aut_G_l4l1_1
(
A
::
LHA
,
S
::
StateLHA
)
=
true
us_aut_G_l4l1_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l1"
;
S
[
"d"
]
+=
S
[
"tprime"
]
*
min
(
abs
(
A
.
l_cte
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
l_cte
s
[
"x2"
]
-
S
[
"n"
]));
S
[
"d"
]
+=
S
[
"tprime"
]
*
min
(
abs
(
A
.
constant
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
constant
s
[
"x2"
]
-
S
[
"n"
]));
S
[
"tprime"
]
=
0.0
;
S
[
"n"
]
=
get_value
(
A
,
x
,
str_obs
);
S
[
"in"
]
=
true
;
...
...
@@ -175,20 +175,20 @@ function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1
tuple
=
(
"l4"
,
"l2"
)
cc_aut_G_l4l2_1
(
A
::
LHA
,
S
::
StateLHA
)
=
(
S
.
time
>=
A
.
l_cte
s
[
"t2"
])
(
S
.
time
>=
A
.
constant
s
[
"t2"
])
us_aut_G_l4l2_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
;
S
[
"d"
]
+=
S
[
"tprime"
]
*
min
(
abs
(
A
.
l_cte
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
l_cte
s
[
"x2"
]
-
S
[
"n"
]));
S
[
"d"
]
+=
S
[
"tprime"
]
*
min
(
abs
(
A
.
constant
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
constant
s
[
"x2"
]
-
S
[
"n"
]));
S
[
"tprime"
]
=
0.0
)
edge1
=
Edge
([
nothing
],
cc_aut_G_l4l2_1
,
us_aut_G_l4l2_1!
)
map_edges
[
tuple
]
=
[
edge1
]
## Constants
l_cte
s
=
Dict
{
String
,
Float64
}(
"x1"
=>
x1
,
"x2"
=>
x2
,
"t1"
=>
t1
,
"t2"
=>
t2
)
constant
s
=
Dict
{
String
,
Float64
}(
"x1"
=>
x1
,
"x2"
=>
x2
,
"t1"
=>
t1
,
"t2"
=>
t2
)
A
=
LHA
(
m
.
l_
transitions
,
l
_loc
,
Λ_F
,
l_loc
_init
,
l_
loc_final
,
map_var_automaton_idx
,
l_
flow
,
map_edges
,
l_cte
s
,
m
.
map_var_idx
)
A
=
LHA
(
m
.
transitions
,
l
ocations
,
Λ_F
,
locations
_init
,
loc
ations
_final
,
map_var_automaton_idx
,
flow
,
map_edges
,
constant
s
,
m
.
map_var_idx
)
return
A
end
...
...
automata/automaton_G_F.jl
View file @
48a39408
...
...
@@ -3,7 +3,7 @@ function create_automaton_G_F(m::ContinuousTimeModel, x1::Float64, x2::Float64,
t1
::
Float64
,
t2
::
Float64
,
t1
::
Float64
,
t2
::
Float64
,
str_obs
::
String
)
@assert
str_obs
in
m
.
g
# Locations
l
_l
oc
=
[
"l0"
,
"l1"
,
"l2"
,
"l3"
,
"l4"
]
loc
ations
=
[
"l0"
,
"l1"
,
"l2"
,
"l3"
,
"l4"
]
# Invariant predicates
true_inv_predicate
=
(
A
::
LHA
,
S
::
StateLHA
)
->
return
true
...
...
@@ -12,15 +12,15 @@ function create_automaton_G_F(m::ContinuousTimeModel, x1::Float64, x2::Float64,
"l4"
=>
true_inv_predicate
)
## Init and final loc
l
_l
oc_init
=
[
"l0"
]
l
_l
oc_final
=
[
"l2"
]
loc
ations
_init
=
[
"l0"
]
loc
ations
_final
=
[
"l2"
]
## Map of automaton variables
map_var_automaton_idx
=
Dict
{
VariableAutomaton
,
Int
}(
"t'"
=>
1
,
"in"
=>
2
,
"n"
=>
3
,
"d"
=>
4
)
## Flow of variables
l_
flow
=
Dict
{
VariableAutomaton
,
Vector
{
Float64
}}(
"l0"
=>
[
0.0
,
0.0
,
0.0
,
0.0
],
flow
=
Dict
{
VariableAutomaton
,
Vector
{
Float64
}}(
"l0"
=>
[
0.0
,
0.0
,
0.0
,
0.0
],
"l1"
=>
[
0.0
,
0.0
,
0.0
,
0.0
],
"l2"
=>
[
0.0
,
0.0
,
0.0
,
0.0
],
"l3"
=>
[
0.0
,
0.0
,
0.0
,
0.0
],
...
...
@@ -41,42 +41,42 @@ function create_automaton_G_F(m::ContinuousTimeModel, x1::Float64, x2::Float64,
# l1 loc
tuple
=
(
"l1"
,
"l3"
)
cc_aut_G_l1l3_1
(
A
::
LHA
,
S
::
StateLHA
)
=
(
S
.
time
<
A
.
l_cte
s
[
"t1"
]
&&
(
S
[
"n"
]
<
A
.
l_cte
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
l_cte
s
[
"x2"
]))
(
S
.
time
<
A
.
constant
s
[
"t1"
]
&&
(
S
[
"n"
]
<
A
.
constant
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
constant
s
[
"x2"
]))
us_aut_G_l1l3_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l3"
;
S
[
"d"
]
=
min
(
abs
(
A
.
l_cte
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
l_cte
s
[
"x2"
]
-
S
[
"n"
]));
S
[
"in"
]
=
false
)
(
S
.
loc
=
"l3"
;
S
[
"d"
]
=
min
(
abs
(
A
.
constant
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
constant
s
[
"x2"
]
-
S
[
"n"
]));
S
[
"in"
]
=
false
)
edge1
=
Edge
([
nothing
],
cc_aut_G_l1l3_1
,
us_aut_G_l1l3_1!
)
cc_aut_G_l1l3_2
(
A
::
LHA
,
S
::
StateLHA
)
=
(
S
.
time
<
A
.
l_cte
s
[
"t1"
]
&&
(
A
.
l_cte
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
l_cte
s
[
"x2"
]))
(
S
.
time
<
A
.
constant
s
[
"t1"
]
&&
(
A
.
constant
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
constant
s
[
"x2"
]))
us_aut_G_l1l3_2!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l3"
;
S
[
"d"
]
=
0
;
S
[
"in"
]
=
false
)
edge2
=
Edge
([
nothing
],
cc_aut_G_l1l3_2
,
us_aut_G_l1l3_2!
)
cc_aut_G_l1l3_3
(
A
::
LHA
,
S
::
StateLHA
)
=
(
!
isin
(
S
[
"in"
])
&&
(
A
.
l_cte
s
[
"t1"
]
<=
S
.
time
<=
A
.
l_cte
s
[
"t2"
])
&&
(
A
.
l_cte
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
l_cte
s
[
"x2"
]))
us_aut_G_l1l3_3!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l3"
;
S
[
"d"
]
=
S
[
"d"
]
*
(
S
.
time
-
A
.
l_cte
s
[
"t1"
]);
S
[
"t'"
]
=
0.0
)
(
!
isin
(
S
[
"in"
])
&&
(
A
.
constant
s
[
"t1"
]
<=
S
.
time
<=
A
.
constant
s
[
"t2"
])
&&
(
A
.
constant
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
constant
s
[
"x2"
]))
us_aut_G_l1l3_3!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l3"
;
S
[
"d"
]
=
S
[
"d"
]
*
(
S
.
time
-
A
.
constant
s
[
"t1"
]);
S
[
"t'"
]
=
0.0
)
edge3
=
Edge
([
nothing
],
cc_aut_G_l1l3_3
,
us_aut_G_l1l3_3!
)
cc_aut_G_l1l3_4
(
A
::
LHA
,
S
::
StateLHA
)
=
(
isin
(
S
[
"in"
])
&&
(
A
.
l_cte
s
[
"t1"
]
<=
S
.
time
<=
A
.
l_cte
s
[
"t2"
])
&&
(
A
.
l_cte
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
l_cte
s
[
"x2"
]))
(
isin
(
S
[
"in"
])
&&
(
A
.
constant
s
[
"t1"
]
<=
S
.
time
<=
A
.
constant
s
[
"t2"
])
&&
(
A
.
constant
s
[
"x1"
]
<=
S
[
"n"
]
<=
A
.
constant
s
[
"x2"
]))
us_aut_G_l1l3_4!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l3"
;
S
[
"t'"
]
=
0.0
)
edge4
=
Edge
([
nothing
],
cc_aut_G_l1l3_4
,
us_aut_G_l1l3_4!
)
map_edges
[
tuple
]
=
[
edge1
,
edge2
,
edge3
,
edge4
]
tuple
=
(
"l1"
,
"l4"
)
cc_aut_G_l1l4_1
(
A
::
LHA
,
S
::
StateLHA
)
=
(
!
isin
(
S
[
"in"
])
&&
(
A
.
l_cte
s
[
"t1"
]
<=
S
.
time
<=
A
.
l_cte
s
[
"t2"
])
&&
(
S
[
"n"
]
<
A
.
l_cte
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
l_cte
s
[
"x2"
]))
us_aut_G_l1l4_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l4"
;
S
[
"d"
]
+=
S
[
"d"
]
*
(
S
.
time
-
A
.
l_cte
s
[
"t1"
]))
(
!
isin
(
S
[
"in"
])
&&
(
A
.
constant
s
[
"t1"
]
<=
S
.
time
<=
A
.
constant
s
[
"t2"
])
&&
(
S
[
"n"
]
<
A
.
constant
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
constant
s
[
"x2"
]))
us_aut_G_l1l4_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l4"
;
S
[
"d"
]
+=
S
[
"d"
]
*
(
S
.
time
-
A
.
constant
s
[
"t1"
]))
edge1
=
Edge
([
nothing
],
cc_aut_G_l1l4_1
,
us_aut_G_l1l4_1!
)
cc_aut_G_l1l4_2
(
A
::
LHA
,
S
::
StateLHA
)
=
(
isin
(
S
[
"in"
])
&&
(
A
.
l_cte
s
[
"t1"
]
<=
S
.
time
<=
A
.
l_cte
s
[
"t2"
])
&&
(
S
[
"n"
]
<
A
.
l_cte
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
l_cte
s
[
"x2"
]))
(
isin
(
S
[
"in"
])
&&
(
A
.
constant
s
[
"t1"
]
<=
S
.
time
<=
A
.
constant
s
[
"t2"
])
&&
(
S
[
"n"
]
<
A
.
constant
s
[
"x1"
]
||
S
[
"n"
]
>
A
.
constant
s
[
"x2"
]))
us_aut_G_l1l4_2!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l4"
)
edge2
=
Edge
([
nothing
],
cc_aut_G_l1l4_2
,
us_aut_G_l1l4_2!
)
map_edges
[
tuple
]
=
[
edge1
,
edge2
]
tuple
=
(
"l1"
,
"l2"
)
cc_aut_G_l1l2_1
(
A
::
LHA
,
S
::
StateLHA
)
=
(
isin
(
S
[
"in"
])
&&
S
.
time
>=
A
.
l_cte
s
[
"t2"
])
cc_aut_G_l1l2_1
(
A
::
LHA
,
S
::
StateLHA
)
=
(
isin
(
S
[
"in"
])
&&
S
.
time
>=
A
.
constant
s
[
"t2"
])
us_aut_G_l1l2_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
)
edge1
=
Edge
([
nothing
],
cc_aut_G_l1l2_1
,
us_aut_G_l1l2_1!
)
cc_aut_G_l1l2_2
(
A
::
LHA
,
S
::
StateLHA
)
=
(
!
isin
(
S
[
"in"
])
&&
S
.
time
>=
A
.
l_cte
s
[
"t2"
])
us_aut_G_l1l2_2!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
;
S
[
"d"
]
=
S
[
"d"
]
*
(
A
.
l_cte
s
[
"t2"
]
-
A
.
l_cte
s
[
"t1"
]))
cc_aut_G_l1l2_2
(
A
::
LHA
,
S
::
StateLHA
)
=
(
!
isin
(
S
[
"in"
])
&&
S
.
time
>=
A
.
constant
s
[
"t2"
])
us_aut_G_l1l2_2!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
;
S
[
"d"
]
=
S
[
"d"
]
*
(
A
.
constant
s
[
"t2"
]
-
A
.
constant
s
[
"t1"
]))
edge2
=
Edge
([
nothing
],
cc_aut_G_l1l2_2
,
us_aut_G_l1l2_2!
)
map_edges
[
tuple
]
=
[
edge1
,
edge2
]
...
...
@@ -88,11 +88,11 @@ function create_automaton_G_F(m::ContinuousTimeModel, x1::Float64, x2::Float64,
map_edges
[
tuple
]
=
[
edge1
]
tuple
=
(
"l3"
,
"l2"
)
cc_aut_G_l3l2_1
(
A
::
LHA
,
S
::
StateLHA
)
=
(
isin
(
S
[
"in"
])
&&
S
.
time
>=
A
.
l_cte
s
[
"t2"
])
cc_aut_G_l3l2_1
(
A
::
LHA
,
S
::
StateLHA
)
=
(
isin
(
S
[
"in"
])
&&
S
.
time
>=
A
.
constant
s
[
"t2"
])
us_aut_G_l3l2_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
)
edge1
=
Edge
([
nothing
],
cc_aut_G_l3l2_1
,
us_aut_G_l3l2_1!
)
cc_aut_G_l3l2_2
(
A
::
LHA
,
S
::
StateLHA
)
=
(
!
isin
(
S
[
"in"
])
&&
S
.
time
>=
A
.
l_cte
s
[
"t2"
])
us_aut_G_l3l2_2!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
;
S
[
"d"
]
=
S
[
"d"
]
*
(
A
.
l_cte
s
[
"t2"
]
-
A
.
l_cte
s
[
"t1"
]))
cc_aut_G_l3l2_2
(
A
::
LHA
,
S
::
StateLHA
)
=
(
!
isin
(
S
[
"in"
])
&&
S
.
time
>=
A
.
constant
s
[
"t2"
])
us_aut_G_l3l2_2!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
;
S
[
"d"
]
=
S
[
"d"
]
*
(
A
.
constant
s
[
"t2"
]
-
A
.
constant
s
[
"t1"
]))
edge2
=
Edge
([
nothing
],
cc_aut_G_l3l2_2
,
us_aut_G_l3l2_2!
)
map_edges
[
tuple
]
=
[
edge1
,
edge2
]
...
...
@@ -100,23 +100,23 @@ function create_automaton_G_F(m::ContinuousTimeModel, x1::Float64, x2::Float64,
tuple
=
(
"l4"
,
"l1"
)
cc_aut_G_l4l1_1
(
A
::
LHA
,
S
::
StateLHA
)
=
true
us_aut_G_l4l1_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l1"
;
S
[
"d"
]
+=
S
[
"t'"
]
*
min
(
abs
(
A
.
l_cte
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
l_cte
s
[
"x2"
]
-
S
[
"n"
]));
(
S
.
loc
=
"l1"
;
S
[
"d"
]
+=
S
[
"t'"
]
*
min
(
abs
(
A
.
constant
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
constant
s
[
"x2"
]
-
S
[
"n"
]));
S
[
"t'"
]
=
0.0
;
S
[
"n"
]
=
get_value
(
A
,
x
,
str_obs
);
S
[
"in"
]
=
true
)
edge1
=
Edge
([
"ALL"
],
cc_aut_G_l4l1_1
,
us_aut_G_l4l1_1!
)
map_edges
[
tuple
]
=
[
edge1
]
tuple
=
(
"l4"
,
"l2"
)
cc_aut_G_l4l2_1
(
A
::
LHA
,
S
::
StateLHA
)
=
(
S
.
time
>=
A
.
l_cte
s
[
"t2"
])
cc_aut_G_l4l2_1
(
A
::
LHA
,
S
::
StateLHA
)
=
(
S
.
time
>=
A
.
constant
s
[
"t2"
])
us_aut_G_l4l2_1!
(
A
::
LHA
,
S
::
StateLHA
,
x
::
Vector
{
Int
})
=
(
S
.
loc
=
"l2"
;
S
[
"d"
]
+=
S
[
"t'"
]
*
min
(
abs
(
A
.
l_cte
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
l_cte
s
[
"x2"
]
-
S
[
"n"
]));
S
[
"t'"
]
=
0.0
)
(
S
.
loc
=
"l2"
;
S
[
"d"
]
+=
S
[
"t'"
]
*
min
(
abs
(
A
.
constant
s
[
"x1"
]
-
S
[
"n"
]),
abs
(
A
.
constant
s
[
"x2"
]
-
S
[
"n"
]));
S
[
"t'"
]
=
0.0
)
edge1
=
Edge
([
nothing
],
cc_aut_G_l4l2_1
,
us_aut_G_l4l2_1!
)
map_edges
[
tuple
]
=
[
edge1
]
## Constants
l_cte
s
=
Dict
{
String
,
Float64
}(
"x1"
=>
x1
,
"x2"
=>
x2
,
"t1"
=>
t1
,
"t2"
=>
t2
)
constant
s
=
Dict
{
String
,
Float64
}(
"x1"
=>
x1
,
"x2"
=>
x2
,
"t1"
=>
t1
,
"t2"
=>
t2
)
A
=
LHA
(
m
.
l_
transitions
,
l
_loc
,
Λ_F
,
l_loc
_init
,
l_
loc_final
,
map_var_automaton_idx
,
l_
flow
,
map_edges
,
l_cte
s
,
m
.
map_var_idx
)
A
=
LHA
(
m
.
transitions
,
l
ocations
,
Λ_F
,
locations
_init
,
loc
ations
_final
,
map_var_automaton_idx
,
flow
,
map_edges
,
constant
s
,
m
.
map_var_idx
)
return
A
end
...
...
core/_tests_simulate.jl
View file @
48a39408
...
...
@@ -29,7 +29,7 @@ _get_value_row(σ::OldTrajectory, var::String, idx::Int) =
function
_simulate_col
(
m
::
ContinuousTimeModel
)
# trajectory fields
full_values
=
zeros
(
m
.
d
,
0
)
full_values
=
zeros
(
m
.
d
im_state
,
0
)
times
=
zeros
(
0
)
transitions
=
Vector
{
Union
{
String
,
Nothing
}}(
undef
,
0
)
# values at time n
...
...
@@ -38,7 +38,7 @@ function _simulate_col(m::ContinuousTimeModel)
tn
=
m
.
t0
tr
=
[
""
]
# at time n+1
xnplus1
=
zeros
(
Int
,
m
.
d
)
xnplus1
=
zeros
(
Int
,
m
.
d
im_state
)
tnplus1
=
zeros
(
Float64
,
1
)
isabsorbing
=
(
m
.
isabsorbing
(
m
.
p
,
xn
))
::
Bool
while
!
isabsorbing
&&
(
tn
<=
m
.
time_bound
)
...
...
@@ -63,7 +63,7 @@ end
function
_simulate_row
(
m
::
ContinuousTimeModel
)
# trajectory fields
full_values
=
zeros
(
m
.
d
,
0
)
full_values
=
zeros
(
m
.
d
im_state
,
0
)
times
=
zeros
(
0
)
transitions
=
Vector
{
Union
{
String
,
Nothing
}}(
undef
,
0
)
# values at time n
...
...
@@ -72,7 +72,7 @@ function _simulate_row(m::ContinuousTimeModel)
tn
=
m
.
t0
tr
=
[
""
]
# at time n+1
xnplus1
=
zeros
(
Int
,
m
.
d
)
xnplus1
=
zeros
(
Int
,
m
.
d
im_state
)
tnplus1
=
zeros
(
Float64
,
1
)
isabsorbing
=
(
m
.
isabsorbing
(
m
.
p
,
xn
))
::
Bool
while
!
isabsorbing
&&
(
tn
<=
m
.
time_bound
)
...
...
@@ -98,7 +98,7 @@ end
function
_simulate_col_buffer
(
m
::
ContinuousTimeModel
;
buffer_size
::
Int
=
5
)
# trajectory fields
full_values
=
zeros
(
m
.
d
,
0
)
full_values
=
zeros
(
m
.
d
im_state
,
0
)
times
=
zeros
(
0
)
transitions
=
Vector
{
Union
{
String
,
Nothing
}}(
undef
,
0
)
# values at time n
...
...
@@ -106,7 +106,7 @@ function _simulate_col_buffer(m::ContinuousTimeModel; buffer_size::Int = 5)
xn
=
@view
m
.
x0
[
:
]
tn
=
m
.
t0
# at time n+1
mat_x
=
zeros
(
Int
,
m
.
d
,
buffer_size
)
mat_x
=
zeros
(
Int
,
m
.
d
im_state
,
buffer_size
)
l_t
=
zeros
(
Float64
,
buffer_size
)
l_tr
=
Vector
{
Union
{
String
,
Nothing
}}(
undef
,
buffer_size
)
isabsorbing
=
m
.
isabsorbing
(
m
.
p
,
xn
)
::
Bool
...
...
@@ -138,7 +138,7 @@ end
function
_simulate_row_buffer
(
m
::
ContinuousTimeModel
;
buffer_size
::
Int
=
5
)
# trajectory fields
full_values
=
zeros
(
0
,
m
.
d
)
full_values
=
zeros
(
0
,
m
.
d
im_state
)
times
=
zeros
(
0
)
transitions
=
Vector
{
Union
{
String
,
Nothing
}}(
undef
,
0
)
# values at time n
...
...
@@ -146,7 +146,7 @@ function _simulate_row_buffer(m::ContinuousTimeModel; buffer_size::Int = 5)
xn
=
@view
m
.
x0
[
:
]
tn
=
m
.
t0
# at time n+1
mat_x
=
zeros
(
Int
,
buffer_size
,
m
.
d
)
mat_x
=
zeros
(
Int
,
buffer_size
,
m
.
d
im_state
)
l_t
=
zeros
(
Float64
,
buffer_size
)
l_tr
=
Vector
{
Union
{
String
,
Nothing
}}(
undef
,
buffer_size
)
isabsorbing
=
m
.
isabsorbing
(
m
.
p
,
xn
)
::
Bool
...
...
@@ -178,7 +178,7 @@ end
function
_simulate_without_view
(
m
::
ContinuousTimeModel
)
# trajectory fields
full_values
=
Matrix
{
Int
}(
undef
,
1
,
m
.
d
)
full_values
=
Matrix
{
Int
}(
undef
,
1
,
m
.
d
im_state
)
full_values
[
1
,
:
]
=
m
.
x0
times
=
Float64
[
m
.
t0
]
transitions
=
Union
{
String
,
Nothing
}[
nothing
]
...
...
@@ -187,7 +187,7 @@ function _simulate_without_view(m::ContinuousTimeModel)
xn
=
@view
m
.
x0
[
:
]
tn
=
m
.
t0
# at time n+1
mat_x
=
zeros
(
Int
,
m
.
buffer_size
,
m
.
d
)
mat_x
=
zeros
(
Int
,
m
.
buffer_size
,
m
.
d
im_state
)
l_t
=
zeros
(
Float64
,
m
.
buffer_size
)
l_tr
=
Vector
{
Union
{
String
,
Nothing
}}(
undef
,
m
.
buffer_size
)
isabsorbing
=
m
.
isabsorbing
(
m
.
p
,
xn
)
::
Bool
...
...
@@ -212,7 +212,7 @@ function _simulate_without_view(m::ContinuousTimeModel)
times
[
end
]
=
m
.
time_bound
transitions
[
end
]
=
nothing
else
full_values
=
vcat
(
full_values
,
reshape
(
full_values
[
end
,
:
],
1
,
m
.
d
))
full_values
=
vcat
(
full_values
,
reshape
(
full_values
[
end
,
:
],
1
,
m
.
d
im_state
))
push!
(
times
,
m
.
time_bound
)
push!
(
transitions
,
nothing
)
end
...
...
@@ -224,16 +224,16 @@ end
# With trajectory values in Matrix type
function
_simulate_27d56
(
m
::
ContinuousTimeModel
)
# trajectory fields
full_values
=
Matrix
{
Int
}(
undef
,
1
,
m
.
d
)
full_values
=
Matrix
{
Int
}(
undef
,
1
,
m
.
d
im_state
)
full_values
[
1
,
:
]
=
m
.
x0
times
=
Float64
[
m
.
t0
]
transitions
=
Union
{
String
,
Nothing
}[
nothing
]
# values at time n
n
=
0
xn
=
view
(
reshape
(
m
.
x0
,
1
,
m
.
d
),
1
,
:
)
# View for type stability
xn
=
view
(
reshape
(
m
.
x0
,
1
,
m
.
d
im_state
),
1
,
:
)
# View for type stability
tn
=
m
.
t0
# at time n+1
mat_x
=
zeros
(
Int
,
m
.
buffer_size
,
m
.
d
)
mat_x
=
zeros
(
Int
,
m
.
buffer_size
,
m
.
d
im_state
)
l_t
=
zeros
(
Float64
,
m
.
buffer_size
)
l_tr
=
Vector
{
Union
{
String
,
Nothing
}}(
undef
,
m
.
buffer_size
)
isabsorbing
::
Bool
=
m
.
isabsorbing
(
m
.
p
,
xn
)
...
...
@@ -265,7 +265,7 @@ function _simulate_27d56(m::ContinuousTimeModel)
else
end
=#
full_values
=
vcat
(
full_values
,
reshape
(
full_values
[
end
,
:
],
1