irafhy
Interval arithmetic based Reachability Analysis Framework for Hybrid Automaton
simple over approximation reach-ability analysis of Helicopter Controller

System

HYBRID_AUTOMATON
{
NAME Helicopter Controller
VARIABLES
{
x1, x2, x3, x4, x5, x6, x7,
x8, x9,x10, x11, x12, x13, x14,
x15, x16, x17, x18, x19,x20, x21,
x22, x23, x24, x25, x26, x27, x28
}
LOCATIONS
{
MODEL
{
NAME controller
FLOWS
{
x1' = 0.998573780060*x4 + 0.053384274244*x5
x2' = 1.000000000000*x3 - 0.003182219341*x4 + 0.059524655342*x5
x3' = -11.570495605469*x3 - 2.544637680054*x4 - 0.063602626324*x5 + 0.106780529022*x6 - 0.094918668270*x7 + 0.007107574493*x8 - 3.700790207851*x9 - 16.213284674534*x10 - 2.984968535139*x11 - 0.493137919288*x12 - 1.186954196152*x13 - 0.031106608756*x14 + 0.024595252653*x15 + 0.008231369923*x16 + 0.231787619674*x17 + 0.745302732591*x18 + 7.895709940231*x19 + 2.026930360369*x20 + 0.271792657736*x21 + 0.315196108541*x22 + 0.015876847710*x23 + 0.009288507454*x24 + 0.087920280806*x25 - 0.103727794204*x26 - 4.447282126346*x27 + 0.016271459306*x28
x4' = 0.439356565475*x3 - 1.998182296753*x4 + 0.016651883721*x6 + 0.018462046981*x7 - 0.001187470742*x8 - 7.517319654181*x9 + 0.236494174025*x10 - 0.028725044803*x11 - 2.442989538035*x12 + 0.034510550810*x13 - 0.004683216652*x14 - 0.005154038690*x15 - 0.002104275246*x16 - 0.079935853309*x17 + 1.420125114638*x18 - 0.117856066698*x19 - 0.226142434271*x20 - 0.002585832387*x21 - 0.001365917341*x22 + 0.035962654791*x23 + 0.028993699893*x24 - 0.045896888864*x25 + 0.716358354284*x26 + 0.029085601036*x27 - 0.001242728387*x28
x5' = -2.040895462036*x3 - 0.458999156952*x4 - 0.735027790070*x5 + 0.019255757332*x6 - 0.004595622420*x7 + 0.002120360732*x8 - 0.740775522612*x9 - 2.555714688932*x10 - 0.339301128908*x11 - 0.033104023297*x12 - 1.446467788369*x13 - 0.007442776396*x14 - 0.000012314482*x15 + 0.030657946816*x16 + 1.002118140789*x17 + 0.153644862643*x18 + 1.273828227991 *x19 + 1.983204935524*x20 + 0.048757213739*x21 + 0.060295617991*x22 + 0.001605314985*x23 + 0.000554368427*x24 + 0.475422075598*x25 - 0.010880647601*x26 - 0.775712358056*x27 - 0.408545111762*x28
x6' = -32.103607177734*x1 - 0.503355026245*x3 + 2.297859191895*x4 - 0.021215811372*x6 - 0.021167919040*x7 + 0.015811592340*x8 + 8.689411857722*x9 - 0.215429806172*x10 + 0.063500560122*x11 + 2.847523923644*x12 - 0.297021616015*x13 + 0.001323463163*x14 + 0.002124820781*x15 + 0.068860932948*x16 + 1.694077894544*x17 - 1.639571645676*x18 + 0.110652545728*x19 + 0.728735301618*x20 + 0.003107735169*x21 + 0.003335187976*x22 - 0.042347579477*x23 - 0.034247794709*x24 + 0.469091132962*x25 - 0.814424502262*x26 - 0.018082452136*x27 + 0.016747349252*x28
x7' = 0.102161169052*x1 + 32.057830810547*x2 - 2.347217559814*x3 - 0.503611564636*x4 + 0.834947586060*x5 + 0.021226570010*x6 - 0.037879735231*x7 + 0.000354003860*x8 - 0.560681623936*x9 - 3.574948145694*x10 - 0.788176766644*x11 - 0.107590635594*x12 + 0.908657075077*x13 - 0.008720966051*x14 + 0.005669792925*x15 + 0.044884407612*x16 + 0.788227489086*x17 + 0.111065913657*x18 + 1.709840089441*x19 - 0.946574755181*x20 + 0.054255711842*x21 + 0.060392345409*x22 + 0.003299051857*x23 + 0.001965592530*x24 - 0.035607238660*x25 - 0.021984114632*x26 - 0.893130060176*x27 + 0.503048977806*x28
x8' = -1.910972595215*x1 + 1.713829040527*x2 - 0.004005432129*x3 - 0.057411193848*x4 + 0.013989634812*x6 - 0.000906753354*x7 - 0.290513515472*x8 - 1.440209153996*x9 - 1.089782421583*x10 - 0.599051729911*x11 - 0.930901394778*x12 + 5.044060722850*x13 + 0.079229241316*x14 + 0.074101747848*x15 - 1.301808243838*x16 - 31.393874531397*x17 + 0.233327947688*x18 + 0.478559456452*x19 - 9.198865975131*x20 - 0.002820980233*x21 - 0.034669033757*x22 + 0.022125233836*x23 + 0.019923408940*x24 - 8.159414332666*x25 - 0.129736796488*x26 - 0.298841506489*x27 - 0.300193732750*x28
x9' = 0.050176870833*x1 - 0.003161246171*x2 - 0.486165175190*x3 + 0.266534777047*x4 + 0.003826227932*x5 + 0.000001339204*x6 + 0.000001199431*x7 - 0.000022435600*x8 - 0.020657323970*x9 + 0.001301453941*x10 + 0.213359280279*x11 + 0.881596311923*x12 + 0.051809053856*x13 - 0.000000551337*x14 - 0.000000493794*x15 + 0.000009236516*x16
x10' = -0.019757788570*x1 + 0.009012833714*x2 + 0.311015942657*x3 + 2.810181204790*x4 - 0.001602140073*x5 - 0.000000613279*x6 - 0.000000549271*x7 + 0.000010274224*x8 + 0.008134087133*x9 - 0.003710494952*x10 + 0.863507011470*x11 - 1.236460821044*x12 + 0.060184240645*x13 + 0.000000252481*x14 + 0.000000226129*x15 - 0.000004229797*x16
x11' = -0.030385323449*x1 + 0.003110159427*x2 + 0.312812882924*x3 + 0.287354391281*x4 - 0.002331730630*x5 - 0.000000824205*x6 - 0.000000738183*x7 + 0.000013807861*x8 - 8.414922645141*x9 - 36.922139523656*x10 - 18.505141519315*x11 - 3.793715804769*x12 - 2.765572372983*x13 + 0.035944961732*x14 - 0.038910104720*x15 + 0.025846348888*x16 + 0.527826299191*x17 + 1.697201876759*x18 + 17.980094722474*x19 + 4.615721721183*x20 + 0.618925691035*x21 + 0.717763941510*x22 + 0.036154725527*x23 + 0.021151770407*x24 + 0.200211885807*x25 - 0.236208723376*x26 - 10.127341872304*x27 + 0.037053334254*x28
x12' = 0.002667394037*x1 + 0.004496152836*x2 + 0.045956750452*x3 + 1.764514260408*x4 + 0.000146052012*x5 + 0.000000019584*x6 + 0.000000017540*x7 - 0.000000328097*x8 - 17.119523267503*x9 + 0.536693033369*x10 + 0.353775293385*x11 - 8.335731095093*x12 + 0.078527228401*x13 + 0.005987264162*x14 + 0.006725273267*x15 - 0.005979187005*x16 - 0.182029763642*x17 + 3.233906041666*x18 - 0.268381596955*x19 - 0.514971094398*x20 - 0.005888452287*x21 - 0.003110464210*x22 + 0.081894084826*x23 + 0.066024394813*x24 - 0.104516302587*x25 + 1.631289796960*x26 + 0.066233671911*x27 - 0.002829938571*x28
x13' = 0.024056576806*x1 - 0.001361685819*x2 - 0.230715295944*x3 + 0.185551143531*x4 + 0.001832537128*x5 + 0.000000640359*x6 + 0.000000573525*x7 - 0.000010727892*x8 - 1.696796379292*x9 - 5.819307733117*x10 - 2.712299197847*x11 - 0.615817527040*x12 - 4.029675752634*x13 + 0.002306818331*x14 - 0.004623901048*x15 + 0.071938991843*x16 + 2.282021405408*x17 + 0.349879770769*x18 + 2.900759066988*x19 + 4.516150272075*x20 + 0.111029828612*x21 + 0.137305059460*x22 + 0.003655620040*x23 + 0.001262406662*x24 + 1.082630189953*x25 - 0.024777388732*x26 - 1.766450614425*x27 - 0.930338103031*x28
x14' = -1.753103616578*x1 + 0.521869609890*x2 + 23.319318958026*x3 + 145.082271971311*x4 - 0.138741289403*x5 - 0.000051341929*x6 - 0.000045983385*x7 + 0.000860128319*x8 - 11.594360544437*x9 - 0.705424902410*x10 - 10.592707880324*x11 - 54.888617486514*x12 - 0.619258600252*x13 - 0.018180886764*x14 - 0.016310350542*x15 + 0.172267463350*x16 + 3.857750758541*x17 - 3.733629238750*x18 + 0.251977753557*x19 + 1.659474556422*x20 + 0.007076928248*x21 + 0.007594883320*x22 - 0.096433822422*x23 - 0.077989008913*x24 + 1.068213380174*x25 - 1.854605830991*x26 - 0.041177323469*x27 + 0.038137029879*x28
x15' = 1.708539622488*x1 + 0.111898315003*x2 - 13.174473231922*x3 + 91.462755556230*x4 + 0.127584976026*x5 + 0.000043171229*x6 + 0.000038665459*x7 - 0.000723245056*x8 - 1.878010842263*x9 + 23.870898681235*x10 + 1.639719754761*x11 - 40.888303474223*x12 + 2.851614162302*x13 + 0.001349430570*x14 - 0.024984412428*x15 + 0.102862439056*x16 + 1.794950045519*x17 + 0.252919074168*x18 + 3.893644396914*x19 - 2.155538119928*x20 + 0.123550997381*x21 + 0.137525326941*x22 + 0.007512594224*x23 + 0.004476043338*x24 - 0.081084731931*x25 - 0.050062181420*x26 - 2.033833968448*x27 + 1.145542115841*x28
x16' = -0.069753861204*x1 + 0.041269247265*x2 + 1.243498527057*x3 + 13.467483657041*x4 - 0.005772466581*x5 - 0.000002269708*x6 - 0.000002032820*x7 + 0.000038024292*x8 - 5.161896992464*x9 - 0.784811430978*x10 - 1.913888711445*x11 - 8.087612492321*x12 + 11.488701354150*x13 + 0.194411237470*x14 + 0.167838434014*x15 - 3.255004272242*x16 - 71.490067651024*x17 + 0.531333931032*x18 + 1.089774627294*x19 - 20.947639012098*x20 - 0.006423930487*x21 - 0.078948253623*x22 + 0.050383537787*x23 + 0.045369546582*x24 - 18.580601832107*x25 - 0.295436370828*x26 - 0.680521274763*x27 - 0.683600561672*x28
x17' = -0.013549327978*x6 - 0.012135188033*x7 + 0.226991094595*x8
x18' = -11.385989897412*x1
x19' = -4.554395958965*x2
x20' = 0.243569095885*x4 - 4.554395958965*x5
x21' = -4.554395958965*x3 - 8.500000000000*x21 - 18.000000000000*x22
x22' = 1.000000000000*x21
x23' = -11.385989897412*x4 - 8.500000000000*x23 - 18.000000000000*x24
x24' = 1.000000000000*x23
x25' = 0.683186075980*x9 + 0.514736886625*x10 + 0.282998565164*x11 + 0.440668616363*x12 - 2.382738811465*x13 - 0.037424700426*x14 - 0.035002491999*x15 + 0.614952694278*x16 + 14.829958398888*x17 - 0.110759742503*x18 - 0.226034186438*x19 + 4.345468653096*x20 + 0.001333027828*x21 + 0.016376955559*x22 - 0.010465240818*x23 - 0.009422482600*x24 - 6.145615181050*x25 + 0.061014181775*x26 + 0.141165339638*x27 + 0.141806743312*x28
x26' = -36.039354729710*x9 + 0.767400874818*x10 - 0.190879388177*x11 - 11.678174370212*x12 - 0.041149877278*x13 - 0.026017271417*x14 - 0.026698725144*x15 + 0.036415219598*x16 + 0.738656358350*x17 + 6.810845841283*x18 - 0.384784957980*x19 - 0.708557300741*x20 - 0.005524328707*x21 + 0.002522572903*x22 + 0.171826920583*x23 + 0.138368426838*x24 + 0.071909684799*x25 - 6.567495145681*x26 + 0.039293511274*x27 + 0.006041152866*x28
x27' = 1.997224587333*x9 + 13.482210983798*x10 + 2.488520358003*x11 + 0.076750797248*x12 + 0.804972334222*x13 + 0.023466195202*x14 - 0.022740687251*x15 + 0.018646161041*x16 + 0.436604617107*x17 - 0.414374632569*x18 - 6.563020897889*x19 - 1.423460802051*x20 - 0.224998971426*x21 - 0.259852011779*x22 - 0.008437464875*x23 - 0.003945344110*x24 + 0.102235829031*x25 + 0.191829027845*x26 - 6.312428841540*x27 - 0.038075090345*x28
x28' = 1.761524247668*x9 - 3.415298165208*x10 - 1.836225244248*x11 - 0.015605131825*x12 + 10.486845595600*x13 - 0.031379180918*x14 + 0.001266746410*x15 + 0.525873993847*x16 + 9.808565668907*x17 - 0.367529750255*x18 + 1.370405524130*x19 - 12.076970057329*x20 + 0.004883176776*x21 - 0.015765473705*x22 - 0.000399777933*x23 - 0.000497333312*x24 + 0.199818976539*x25 - 0.002648145523*x26 - 0.101212258081*x27 - 5.199268943788*x28
}
INVARIANT_CONDITIONS
{
}
}
}
TRANSITIONS
{
}
}

Setting

SETTINGS
{
TIME_HORIZON := [0,30]
STEP := 0.1
GEOMETRY := INTERVAL_HULL
PLOT := ON
PRINT := OFF
ANALYSIS := FORWARD
MAX_JUMP := 1
START_MODEL_ID := controller #name of the model
INITIAL_CONDITION :=
CONDITION
{
INTERVAL_HULL
{
[0.0,0.1],
[0.0,0.1],
[0.0,0.1],
[0.0,0.1],
[0.0,0.1],
[0.0,0.1],
[0.0,0.1],
[0.0,0.1],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0],
[0.0,0.0]
}
}
}

Result

here are some screenshots of the results

3d
0
1
2