lpsinvelm - ക്ലൗഡിൽ ഓൺലൈനിൽ

പട്ടിക:

NAME

lpsinvelm - വ്യതിയാനങ്ങൾ പരിശോധിച്ച് ഒരു LPS-ന്റെ സംഗ്രഹങ്ങൾ ലഘൂകരിക്കാനോ ഇല്ലാതാക്കാനോ ഇവ ഉപയോഗിക്കുക

സിനോപ്സിസ്

lpsinvelm [ഓപ്ഷൻ]... --invfile=INVFILE [INFILE [ഔട്ട്ഫിൽ]]

വിവരണം

ബൂളിയൻ ഫോർമുല (ബൂളിന്റെ ഒരു mCRL2 ഡാറ്റ എക്സ്പ്രഷൻ) ഇപ്രകാരം നൽകിയിട്ടുണ്ടോയെന്ന് പരിശോധിക്കുന്നു
INFILE-ലെ ലീനിയർ പ്രോസസ് സ്പെസിഫിക്കേഷന്റെ (LPS) ഒരു മാറ്റമാണ് invariant. ഇതാണെങ്കിൽ
സാഹചര്യം ലംഘിക്കുന്ന LPS-ന്റെ എല്ലാ സമ്മൻഡുകളും ഉപകരണം ഇല്ലാതാക്കുന്നു
മാറ്റമില്ലാത്തത്, ഫലം OUTFILE-ലേക്ക് എഴുതുന്നു. INFILE ഉണ്ടെങ്കിൽ, stdin ഉപയോഗിക്കുന്നു. എങ്കിൽ
OUTFILE നിലവിലില്ല, stdout ഉപയോഗിക്കുന്നു.

തന്നിരിക്കുന്ന LPS-ന്റെ സംഗ്രഹങ്ങളുടെ വ്യവസ്ഥകൾ ലളിതമാക്കുന്നതിനും ഈ ഉപകരണം ഉപയോഗിക്കാവുന്നതാണ്.

ഓപ്ഷനുകൾ

ഓപ്ഷൻ ഇനിപ്പറയുന്നവയിൽ ഏതെങ്കിലും ആകാം:

-y, --എല്ലാ-ലംഘനങ്ങളും
മാറ്റമില്ലാത്തതിന്റെ ഒരൊറ്റ ലംഘനം കണ്ടെത്തിയാലുടൻ അവസാനിപ്പിക്കരുത്, പക്ഷേ
പകരം എല്ലാ ലംഘനങ്ങളും റിപ്പോർട്ട് ചെയ്യുക

-c, --പ്രതി-ഉദാഹരണം
മാറ്റമില്ലാത്തത് എന്തുകൊണ്ട് ലംഘിക്കപ്പെടാം എന്ന് സൂചിപ്പിക്കുന്ന ഒരു മൂല്യനിർണ്ണയം പ്രദർശിപ്പിക്കുക
ഒരു സമാൻഡ് മാറ്റമില്ലാത്തതിനെ ലംഘിക്കുന്നുണ്ടോ എന്ന് ഉറപ്പില്ല

-o, --ഇൻഡക്ഷൻ
ലിസ്റ്റുകളിൽ ഇൻഡക്ഷൻ പ്രയോഗിക്കുക

-iINVFILE, --മാറ്റമില്ലാത്ത=INVFILE
INVFILE-ൽ ബൂളിയൻ ഫോർമുല (ഒരു mCRL2 ഡാറ്റാ എക്സ്പ്രഷൻ ബൂൾ) ഉപയോഗിക്കുക
മാറ്റമില്ലാത്ത

-n, --നോ-ചെക്ക്
എത്തിച്ചേരാനാകാത്ത സമ്മണ്ടുകൾ ഇല്ലാതാക്കുന്നതിന് മുമ്പ് മാറ്റമില്ലാത്തത് കൈവശം വച്ചിട്ടുണ്ടോ എന്ന് പരിശോധിക്കരുത്

-e, --എലിമിനേഷൻ ഇല്ല
സംഗ്രഹങ്ങൾ ഇല്ലാതാക്കുകയോ ലളിതമാക്കുകയോ ചെയ്യരുത്, എന്നാൽ ഓരോ വ്യവസ്ഥയിലും മാറ്റമില്ലാത്തത് ചേർക്കുക

-pപ്രിഫിക്‌സ്, --പ്രിന്റ്-ഡോട്ട്=പ്രിഫിക്‌സ്
a എന്ന് നിർണ്ണയിക്കാൻ കഴിയുന്നില്ലെങ്കിൽ, തത്ഫലമായുണ്ടാകുന്ന BDD-യുടെ ഒരു .dot ഫയൽ സംരക്ഷിക്കുക
സംമാൻഡ് മാറ്റമില്ലാത്തതിനെ ലംഘിക്കുന്നു; ഔട്ട്‌പുട്ട് ഫയലുകളുടെ പ്രിഫിക്‌സായി PREFIX ഉപയോഗിക്കും

-QNUMBER, --ക്ലിമിറ്റ്=NUMBER
ക്വാണ്ടിഫയറുകളുടെ എണ്ണം NUM വേരിയബിളുകളായി പരിമിതപ്പെടുത്തുക. (ഡിഫോൾട്ട് NUM=1000, NUM=0 ഇതിനായി
പരിധിയില്ലാത്തത്).

-rNAME, --റീറൈറ്റർ=NAME
റീറൈറ്റിംഗ് സ്ട്രാറ്റജി ഉപയോഗിക്കുക
jitty rewriting 'jittyp' ജിട്ടി തിരുത്തിയെഴുതുന്നു

-l, --എല്ലാം ലളിതമാക്കുക
സംഗ്രഹങ്ങൾ ഒഴിവാക്കുന്നതിനുപകരം എല്ലാ സംഗ്രഹങ്ങളുടെയും വ്യവസ്ഥകൾ ലളിതമാക്കുക
മാറ്റമില്ലാത്തവയുമായി ചേർന്നുള്ള വ്യവസ്ഥകൾ വൈരുദ്ധ്യങ്ങളാണ്

-zസോൾവർ, --smt-solver=സോൾവർ
ആന്തരികമായി ഉപയോഗിക്കുന്ന BDD-കളിൽ നിന്ന് പൊരുത്തമില്ലാത്ത പാതകൾ നീക്കം ചെയ്യാൻ SOLVER ഉപയോഗിക്കുക (സ്ഥിരസ്ഥിതിയായി,
പാത്ത് എലിമിനേഷൻ ബാധകമല്ല): SMT സോൾവർ CVC3 'cvc'

-tപരിധി, --സമയ പരിധി=പരിധി
ഒരൊറ്റ ഫോർമുല തെളിയിക്കാൻ പരമാവധി LIMIT സെക്കൻഡ് ചെലവഴിക്കുക

--സമയങ്ങൾ[=FILE]
FILE-ലേക്ക് സമയ അളവുകൾ കൂട്ടിച്ചേർക്കുക. എങ്കിൽ അളവുകൾ സാധാരണ പിശകിന് എഴുതിയിരിക്കുന്നു
ഫയലൊന്നും നൽകിയിട്ടില്ല

സ്റ്റാൻഡേർഡ് ഓപ്ഷനുകൾ:

-q, --നിശബ്ദമായി
മുന്നറിയിപ്പ് സന്ദേശങ്ങൾ പ്രദർശിപ്പിക്കരുത്

-v, --വാക്കുകൾ
ഹ്രസ്വമായ ഇന്റർമീഡിയറ്റ് സന്ദേശങ്ങൾ പ്രദർശിപ്പിക്കുക

-d, --ഡീബഗ്
വിശദമായ ഇന്റർമീഡിയറ്റ് സന്ദേശങ്ങൾ പ്രദർശിപ്പിക്കുക

--ലോഗ്-ലെവൽ=ലെവൽ
ലെവൽ ഉൾപ്പെടെയുള്ള ഇന്റർമീഡിയറ്റ് സന്ദേശങ്ങൾ പ്രദർശിപ്പിക്കുക

-h, --സഹായിക്കൂ
സഹായ വിവരങ്ങൾ പ്രദർശിപ്പിക്കുക

--പതിപ്പ്
പതിപ്പ് വിവരങ്ങൾ പ്രദർശിപ്പിക്കുക

onworks.net സേവനങ്ങൾ ഉപയോഗിച്ച് lpsinvelm ഓൺലൈനായി ഉപയോഗിക്കുക